Dave is big. Dave is cold. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Gary is cold. Gary is quiet. Gary is rough. Cold things are smart. All rough, big things are kind. Quiet things are rough. All rough, smart things are big. If something is cold and round then it is kind. If Dave is big then Dave is kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All rough, big things are kind.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All rough, smart things are big.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is cold and round then it is kind.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Dave is big then Dave is kind.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
Dave is smart.
True
1
proof
[(triple7 OR ((triple2) -> rule1))]
("Dave" "is" "smart" "+")
triple7
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is not quiet.
False
1
inv-proof
[(triple9)]
("Gary" "is" "quiet" "-")
triple9
Gary is smart.
True
2
proof
[(((triple8) -> rule1))]
("Gary" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Gary" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
True
4
proof
[(((triple10 ((triple8) -> rule1)) -> rule4) OR ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4))]
("Gary" "is" "big" "+")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not big.
False
4
inv-proof
[(((triple10 ((triple8) -> rule1)) -> rule4) OR ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4))]
("Gary" "is" "big" "-")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
True
6
proof
[(((triple10 ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((triple10 ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2))]
("Gary" "is" "kind" "+")
((triple10 ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple10 ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not kind.
False
6
inv-proof
[(((triple10 ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((triple10 ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2))]
("Gary" "is" "kind" "-")
((triple10 ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple10 ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
@0: Dave is big.[(triple1 OR ((triple5 triple7) -> rule4) OR ((triple5 ((triple2) -> rule1)) -> rule4) OR ((((triple4) -> rule3) triple7) -> rule4) OR ((((triple4) -> rule3) ((triple2) -> rule1)) -> rule4))] Dave is cold.[(triple2)] Dave is kind.[(triple3 OR ((triple1) -> rule6) OR ((triple2 triple6) -> rule5) OR ((triple5 triple1) -> rule2) OR ((((triple5 triple7) -> rule4)) -> rule6) OR ((triple5 ((triple5 triple7) -> rule4)) -> rule2) OR ((((triple4) -> rule3) triple1) -> rule2) OR ((((triple4) -> rule3) ((triple5 triple7) -> rule4)) -> rule2) OR ((((triple5 ((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple4) -> rule3) triple7) -> rule4)) -> rule6) OR ((triple5 ((triple5 ((triple2) -> rule1)) -> rule4)) -> rule2) OR ((triple5 ((((triple4) -> rule3) triple7) -> rule4)) -> rule2) OR ((((((triple4) -> rule3) ((triple2) -> rule1)) -> rule4)) -> rule6) OR ((triple5 ((((triple4) -> rule3) ((triple2) -> rule1)) -> rule4)) -> rule2) OR ((((triple4) -> rule3) ((triple5 ((triple2) -> rule1)) -> rule4)) -> rule2) OR ((((triple4) -> rule3) ((((triple4) -> rule3) triple7) -> rule4)) -> rule2) OR ((((triple4) -> rule3) ((((triple4) -> rule3) ((triple2) -> rule1)) -> rule4)) -> rule2))] Dave is quiet.[(triple4)] Dave is rough.[(triple5 OR ((triple4) -> rule3))] Dave is round.[(triple6)] Dave is smart.[(triple7 OR ((triple2) -> rule1))] Gary is cold.[(triple8)] Gary is quiet.[(triple9)] Gary is rough.[(triple10 OR ((triple9) -> rule3))] @1: Gary is smart.[(((triple8) -> rule1))] @2: Gary is big.[(((triple10 ((triple8) -> rule1)) -> rule4) OR ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4))] @3: Gary is kind.[(((triple10 ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((triple10 ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((triple10 ((triple8) -> rule1)) -> rule4)) -> rule2) OR ((((triple9) -> rule3) ((((triple9) -> rule3) ((triple8) -> rule1)) -> rule4)) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple5 triple7) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple5 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple4) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple1) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple2 triple6) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple5 triple1) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple5 triple7) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple5 ((triple5 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple5 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple5 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple4) -> (rule3 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple5 ((triple5 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple5 ((((triple4) -> (rule3 % int3)) triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple4) -> (rule3 % int4)) ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((triple5 ((((triple4) -> (rule3 % int4)) ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple4) -> (rule3 % int4)) ((triple5 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3)) triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple4) -> (rule3 % int4)) ((((triple4) -> (rule3 % int4)) ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple9) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((triple10 ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple10 ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
((((triple9) -> (rule3 % int4)) ((((triple9) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4