Charlie is big. Charlie is blue. Charlie is cold. Charlie is green. Charlie is nice. Charlie is young. Fiona is big. Fiona is blue. Fiona is cold. Fiona is green. Fiona is nice. Fiona is round. Fiona is young. Gary is cold. Gary is nice. Gary is young. If Charlie is nice and Charlie is blue then Charlie is round. Big things are round. All nice things are blue. All big things are green. If something is nice and blue then it is big. Green things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
If Charlie is nice and Charlie is blue then Charlie is round.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "round" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is nice and blue then it is big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Charlie is big.
True
1
proof
[(triple1 OR ((triple4) -> rule6) OR ((triple5 triple2) -> rule5) OR ((triple5 ((triple5) -> rule3)) -> rule5))]
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Fiona is not cold.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "cold" "-")
triple9
Charlie is round.
True
2
proof
[(((triple1) -> rule2) OR ((triple5 triple2) -> rule1) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple5 triple2) -> rule5)) -> rule2) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5 ((triple5) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple5 triple2) -> rule1) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple5 triple2) -> rule5)) -> rule2) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5 ((triple5) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "round" "-")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Gary is big.
True
4
proof
[(((triple15 ((triple15) -> rule3)) -> rule5))]
("Gary" "is" "big" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
False
4
inv-proof
[(((triple15 ((triple15) -> rule3)) -> rule5))]
("Gary" "is" "big" "-")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
True
5
proof
[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "round" "+")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not green.
False
5
inv-proof
[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4))]
("Gary" "is" "green" "-")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
@0: Charlie is big.[(triple1 OR ((triple4) -> rule6) OR ((triple5 triple2) -> rule5) OR ((triple5 ((triple5) -> rule3)) -> rule5))] Charlie is blue.[(triple2 OR ((triple5) -> rule3))] Charlie is cold.[(triple3)] Charlie is green.[(triple4 OR ((triple1) -> rule4) OR ((((triple5 triple2) -> rule5)) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule5)) -> rule4))] Charlie is nice.[(triple5)] Charlie is young.[(triple6)] Fiona is big.[(triple7 OR ((triple10) -> rule6) OR ((triple11 triple8) -> rule5) OR ((triple11 ((triple11) -> rule3)) -> rule5))] Fiona is blue.[(triple8 OR ((triple11) -> rule3))] Fiona is cold.[(triple9)] Fiona is green.[(triple10 OR ((triple7) -> rule4) OR ((((triple11 triple8) -> rule5)) -> rule4) OR ((((triple11 ((triple11) -> rule3)) -> rule5)) -> rule4))] Fiona is nice.[(triple11)] Fiona is round.[(triple12 OR ((triple7) -> rule2) OR ((((triple10) -> rule6)) -> rule2) OR ((((triple11 triple8) -> rule5)) -> rule2) OR ((((triple11 ((triple11) -> rule3)) -> rule5)) -> rule2))] Fiona is young.[(triple13)] Gary is cold.[(triple14)] Gary is nice.[(triple15)] Gary is young.[(triple16)] @1: Charlie is round.[(((triple1) -> rule2) OR ((triple5 triple2) -> rule1) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple5 triple2) -> rule5)) -> rule2) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5 ((triple5) -> rule3)) -> rule5)) -> rule2))] Gary is blue.[(((triple15) -> rule3))] @2: Gary is big.[(((triple15 ((triple15) -> rule3)) -> rule5))] @3: Gary is green.[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4))] Gary is round.[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple5) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple1) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple5 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple10) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple11 triple8) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple11 ((triple11) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple11) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple11 triple8) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple11 ((triple11) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple7) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple11 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple11 ((triple11) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((triple15) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3