Anne is big. Anne is kind. Anne is rough. Anne is smart. Charlie is big. Charlie is cold. Charlie is kind. Charlie is rough. Charlie is round. Charlie is young. All big, cold things are round. Young things are cold. Round, kind things are smart. If Charlie is rough then Charlie is young. Kind things are young. If Anne is big and Anne is smart then Anne is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All big, cold things are round.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Round, kind things are smart.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Charlie is rough then Charlie is young.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Anne is big and Anne is smart then Anne is young.
((("Anne" "is" "big" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
Charlie is round.
True
1
proof
[(triple9 OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple10) -> rule2)) -> rule1) OR ((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule1) OR ((triple5 ((((triple8) -> rule4)) -> rule2)) -> rule1))]
("Charlie" "is" "round" "+")
triple9
((triple5 triple6) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((triple5 ((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not kind.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "kind" "-")
triple7
Anne is young.
True
2
proof
[(((triple2) -> rule5) OR ((triple1 triple4) -> rule6))]
("Anne" "is" "young" "+")
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple1 triple4) -> rule6))]
("Anne" "is" "young" "-")
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
True
3
proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple1 triple4) -> rule6)) -> rule2))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple1 triple4) -> rule6)) -> rule2))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
True
5
proof
[(((triple1 ((((triple2) -> rule5)) -> rule2)) -> rule1) OR ((triple1 ((((triple1 triple4) -> rule6)) -> rule2)) -> rule1))]
("Anne" "is" "round" "+")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple1 ((((triple1 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not round.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule5)) -> rule2)) -> rule1) OR ((triple1 ((((triple1 triple4) -> rule6)) -> rule2)) -> rule1))]
("Anne" "is" "round" "-")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple1 ((((triple1 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4 OR ((((triple1 ((((triple2) -> rule5)) -> rule2)) -> rule1) triple2) -> rule3))] Charlie is big.[(triple5)] Charlie is cold.[(triple6 OR ((triple10) -> rule2) OR ((((triple7) -> rule5)) -> rule2) OR ((((triple8) -> rule4)) -> rule2))] Charlie is kind.[(triple7)] Charlie is rough.[(triple8)] Charlie is round.[(triple9 OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple10) -> rule2)) -> rule1) OR ((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule1) OR ((triple5 ((((triple8) -> rule4)) -> rule2)) -> rule1))] Charlie is young.[(triple10 OR ((triple7) -> rule5) OR ((triple8) -> rule4))] @1: Anne is young.[(((triple2) -> rule5) OR ((triple1 triple4) -> rule6))] Charlie is smart.[(((triple9 triple7) -> rule3) OR ((((triple5 triple6) -> rule1) triple7) -> rule3) OR ((((triple5 ((triple10) -> rule2)) -> rule1) triple7) -> rule3) OR ((((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule1) triple7) -> rule3) OR ((((triple5 ((((triple8) -> rule4)) -> rule2)) -> rule1) triple7) -> rule3))] @2: Anne is cold.[(((((triple2) -> rule5)) -> rule2) OR ((((triple1 triple4) -> rule6)) -> rule2))] @3: Anne is round.[(((triple1 ((((triple2) -> rule5)) -> rule2)) -> rule1) OR ((triple1 ((((triple1 triple4) -> rule6)) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((((triple1 ((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((triple10) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
((triple5 triple6) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((triple5 ((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple10
((triple7) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple8) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple9 triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple5 triple6) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple5 ((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple5 ((((triple7) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((triple5 ((((triple8) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple1 ((((triple1 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3