Charlie is big. Charlie is blue. Charlie is cold. Charlie is kind. Charlie is rough. Charlie is round. Charlie is white. Harry is big. Harry is blue. Harry is cold. Harry is kind. Harry is rough. Harry is round. Harry is white. All white things are blue. If something is big then it is white. All round, cold things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
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 white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All round, cold things are big.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple13)]
("Harry" "is" "round" "+")
triple13
Harry is not kind.
False
1
inv-proof
[(triple11)]
("Harry" "is" "kind" "-")
triple11
@0: Charlie is big.[(triple1 OR ((triple6 triple3) -> rule3))] Charlie is blue.[(triple2 OR ((triple7) -> rule1) OR ((((triple1) -> rule2)) -> rule1) OR ((((((triple6 triple3) -> rule3)) -> rule2)) -> rule1))] Charlie is cold.[(triple3)] Charlie is kind.[(triple4)] Charlie is rough.[(triple5)] Charlie is round.[(triple6)] Charlie is white.[(triple7 OR ((triple1) -> rule2) OR ((((triple6 triple3) -> rule3)) -> rule2))] Harry is big.[(triple8 OR ((triple13 triple10) -> rule3))] Harry is blue.[(triple9 OR ((triple14) -> rule1) OR ((((triple8) -> rule2)) -> rule1) OR ((((((triple13 triple10) -> rule3)) -> rule2)) -> rule1))] Harry is cold.[(triple10)] Harry is kind.[(triple11)] Harry is rough.[(triple12)] Harry is round.[(triple13)] Harry is white.[(triple14 OR ((triple8) -> rule2) OR ((((triple13 triple10) -> rule3)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple6 triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple6 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple6 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple13 triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
((triple14) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple13 triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
((triple8) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple13 triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2