Charlie is big. Charlie is kind. Charlie is smart. Charlie is white. Dave is big. Dave is blue. Dave is cold. Dave is kind. Dave is round. Dave is smart. Dave is white. Fiona is blue. Fiona is cold. Fiona is kind. Fiona is smart. If someone is white and big then they are smart. Blue, kind people are cold. If someone is smart and cold then they are big. All kind people are blue. If someone is cold then they are round. If Dave is smart and Dave is white then Dave is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is white and big then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Blue, kind people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and cold then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart and Dave is white then Dave is big.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "big" "+"))
Dave is blue.
True
1
proof
[(triple6 OR ((triple8) -> rule4))]
("Dave" "is" "blue" "+")
triple6
((triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple9 OR ((triple7) -> rule5) OR ((((triple6 triple8) -> rule2)) -> rule5) OR ((((((triple8) -> rule4) triple8) -> rule2)) -> rule5))]
("Dave" "is" "round" "-")
triple9
((triple7) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple8) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Fiona is round.
True
2
proof
[(((triple13) -> rule5) OR ((((triple12 triple14) -> rule2)) -> rule5) OR ((((((triple14) -> rule4) triple14) -> rule2)) -> rule5))]
("Fiona" "is" "round" "+")
((triple13) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple12 triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple14) -> (rule4 % int3)) triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not round.
False
2
inv-proof
[(((triple13) -> rule5) OR ((((triple12 triple14) -> rule2)) -> rule5) OR ((((((triple14) -> rule4) triple14) -> rule2)) -> rule5))]
("Fiona" "is" "round" "-")
((triple13) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple12 triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple14) -> (rule4 % int3)) triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Charlie is cold.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("Charlie" "is" "cold" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not cold.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("Charlie" "is" "cold" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
("Charlie" "is" "round" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not round.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
("Charlie" "is" "round" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
@0: Charlie is big.[(triple1 OR ((triple3 ((((triple2) -> rule4) triple2) -> rule2)) -> rule3))] Charlie is kind.[(triple2)] Charlie is smart.[(triple3 OR ((triple4 triple1) -> rule1))] Charlie is white.[(triple4)] Dave is big.[(triple5 OR ((triple10 triple11) -> rule6) OR ((triple10 triple7) -> rule3) OR ((triple10 ((triple6 triple8) -> rule2)) -> rule3) OR ((triple10 ((((triple8) -> rule4) triple8) -> rule2)) -> rule3))] Dave is blue.[(triple6 OR ((triple8) -> rule4))] Dave is cold.[(triple7 OR ((triple6 triple8) -> rule2) OR ((((triple8) -> rule4) triple8) -> rule2))] Dave is kind.[(triple8)] Dave is round.[(triple9 OR ((triple7) -> rule5) OR ((((triple6 triple8) -> rule2)) -> rule5) OR ((((((triple8) -> rule4) triple8) -> rule2)) -> rule5))] Dave is smart.[(triple10 OR ((triple11 triple5) -> rule1))] Dave is white.[(triple11)] Fiona is blue.[(triple12 OR ((triple14) -> rule4))] Fiona is cold.[(triple13 OR ((triple12 triple14) -> rule2) OR ((((triple14) -> rule4) triple14) -> rule2))] Fiona is kind.[(triple14)] Fiona is smart.[(triple15)] @1: Charlie is blue.[(((triple2) -> rule4))] Fiona is big.[(((triple15 triple13) -> rule3) OR ((triple15 ((triple12 triple14) -> rule2)) -> rule3) OR ((triple15 ((((triple14) -> rule4) triple14) -> rule2)) -> rule3))] Fiona is round.[(((triple13) -> rule5) OR ((((triple12 triple14) -> rule2)) -> rule5) OR ((((((triple14) -> rule4) triple14) -> rule2)) -> rule5))] @2: Charlie is cold.[(((((triple2) -> rule4) triple2) -> rule2))] @3: Charlie is round.[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 ((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple4 triple1) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple10 triple11) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple10 triple7) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple10 ((triple6 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple10 ((((triple8) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple7
((triple6 triple8) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple8) -> (rule4 % int2)) triple8) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple7) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple8) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple10
((triple11 triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple11
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
((triple14) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple13
((triple12 triple14) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple14) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple15 triple13) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple15 ((triple12 triple14) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple15 ((((triple14) -> (rule4 % int3)) triple14) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((triple13) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple12 triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple14) -> (rule4 % int3)) triple14) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3