Gary is big. Gary is blue. Gary is cold. Gary is quiet. Gary is rough. Gary is smart. Gary is white. Harry is big. Harry is blue. Harry is quiet. Harry is smart. Harry is white. If Gary is white then Gary is blue. If Harry is smart and Harry is blue then Harry is white. Cold things are big. Quiet, white things are smart. All rough, smart things are cold. All cold things are rough. Quiet things are rough. Blue, quiet things are white.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is white then Gary is blue.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "blue" "+"))
If Harry is smart and Harry is blue then Harry is white.
((("Harry" "is" "smart" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "white" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Quiet, white things are smart.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All rough, smart things are cold.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Blue, quiet things are white.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Harry is big.
True
1
proof
[(triple8 OR ((((((triple10) -> rule7) triple11) -> rule5)) -> rule3) OR ((((((triple10) -> rule7) ((triple10 triple12) -> rule4)) -> rule5)) -> rule3) OR ((((((triple10) -> rule7) ((triple10 ((triple9 triple10) -> rule8)) -> rule4)) -> rule5)) -> rule3))]
("Harry" "is" "big" "+")
triple8
((((((triple10) -> (rule7 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple10) -> (rule7 % int4)) ((triple10 triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple10) -> (rule7 % int5)) ((triple10 ((triple9 triple10) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is not quiet.
False
1
inv-proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Harry is rough.
True
2
proof
[(((triple10) -> rule7))]
("Harry" "is" "rough" "+")
((triple10) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple10) -> rule7))]
("Harry" "is" "rough" "-")
((triple10) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
True
4
proof
[(((((triple10) -> rule7) triple11) -> rule5) OR ((((triple10) -> rule7) ((triple10 triple12) -> rule4)) -> rule5) OR ((((triple10) -> rule7) ((triple10 ((triple9 triple10) -> rule8)) -> rule4)) -> rule5))]
("Harry" "is" "cold" "+")
((((triple10) -> (rule7 % int2)) triple11) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple10) -> (rule7 % int3)) ((triple10 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10) -> (rule7 % int4)) ((triple10 ((triple9 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not cold.
False
4
inv-proof
[(((((triple10) -> rule7) triple11) -> rule5) OR ((((triple10) -> rule7) ((triple10 triple12) -> rule4)) -> rule5) OR ((((triple10) -> rule7) ((triple10 ((triple9 triple10) -> rule8)) -> rule4)) -> rule5))]
("Harry" "is" "cold" "-")
((((triple10) -> (rule7 % int2)) triple11) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple10) -> (rule7 % int3)) ((triple10 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10) -> (rule7 % int4)) ((triple10 ((triple9 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
@0: Gary is big.[(triple1 OR ((triple3) -> rule3) OR ((((triple5 triple6) -> rule5)) -> rule3) OR ((((triple5 ((triple4 triple7) -> rule4)) -> rule5)) -> rule3) OR ((((((triple4) -> rule7) triple6) -> rule5)) -> rule3) OR ((((((triple4) -> rule7) ((triple4 triple7) -> rule4)) -> rule5)) -> rule3) OR ((((triple5 ((triple4 ((triple2 triple4) -> rule8)) -> rule4)) -> rule5)) -> rule3) OR ((((((triple4) -> rule7) ((triple4 ((triple2 triple4) -> rule8)) -> rule4)) -> rule5)) -> rule3))] Gary is blue.[(triple2 OR ((triple7) -> rule1))] Gary is cold.[(triple3 OR ((triple5 triple6) -> rule5) OR ((triple5 ((triple4 triple7) -> rule4)) -> rule5) OR ((((triple4) -> rule7) triple6) -> rule5) OR ((((triple4) -> rule7) ((triple4 triple7) -> rule4)) -> rule5) OR ((triple5 ((triple4 ((triple2 triple4) -> rule8)) -> rule4)) -> rule5) OR ((((triple4) -> rule7) ((triple4 ((triple2 triple4) -> rule8)) -> rule4)) -> rule5))] Gary is quiet.[(triple4)] Gary is rough.[(triple5 OR ((triple3) -> rule6) OR ((triple4) -> rule7))] Gary is smart.[(triple6 OR ((triple4 triple7) -> rule4) OR ((triple4 ((triple2 triple4) -> rule8)) -> rule4))] Gary is white.[(triple7 OR ((triple2 triple4) -> rule8))] Harry is big.[(triple8 OR ((((((triple10) -> rule7) triple11) -> rule5)) -> rule3) OR ((((((triple10) -> rule7) ((triple10 triple12) -> rule4)) -> rule5)) -> rule3) OR ((((((triple10) -> rule7) ((triple10 ((triple9 triple10) -> rule8)) -> rule4)) -> rule5)) -> rule3))] Harry is blue.[(triple9)] Harry is quiet.[(triple10)] Harry is smart.[(triple11 OR ((triple10 triple12) -> rule4) OR ((triple10 ((triple9 triple10) -> rule8)) -> rule4))] Harry is white.[(triple12 OR ((triple11 triple9) -> rule2) OR ((triple9 triple10) -> rule8))] @1: Harry is rough.[(((triple10) -> rule7))] @2: Harry is cold.[(((((triple10) -> rule7) triple11) -> rule5) OR ((((triple10) -> rule7) ((triple10 triple12) -> rule4)) -> rule5) OR ((((triple10) -> rule7) ((triple10 ((triple9 triple10) -> rule8)) -> rule4)) -> rule5))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple5 ((triple4 triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((triple4) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple4) -> (rule7 % int4)) ((triple4 triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple5 ((triple4 ((triple2 triple4) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((triple4) -> (rule7 % int5)) ((triple4 ((triple2 triple4) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is blue.
("Gary" "is" "blue" "+")
triple2
((triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple3
((triple5 triple6) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple5 ((triple4 triple7) -> (rule4 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple4) -> (rule7 % int2)) triple6) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4 triple7) -> (rule4 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((triple5 ((triple4 ((triple2 triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple4) -> (rule7 % int4)) ((triple4 ((triple2 triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple4 triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple4 ((triple2 triple4) -> (rule8 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple2 triple4) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
((((((triple10) -> (rule7 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple10) -> (rule7 % int4)) ((triple10 triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple10) -> (rule7 % int5)) ((triple10 ((triple9 triple10) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple10 triple12) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 ((triple9 triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple11 triple9) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 triple10) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple10) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple10) -> (rule7 % int2)) triple11) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple10) -> (rule7 % int3)) ((triple10 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10) -> (rule7 % int4)) ((triple10 ((triple9 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4