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