Bob is green. Bob is white. Dave is quiet. Dave is smart. Erin is quiet. Erin is round. Gary is cold. Gary is quiet. Gary is round. Gary is smart. All round, green people are smart. Round people are white. All green people are cold. Quiet people are big. If Gary is white then Gary is green. Smart, big people are green. If Gary is green and Gary is white then Gary is cold. Quiet, cold people are round.
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All round, green people are smart.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Gary is white then Gary is green.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
Smart, big people are green.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Gary is green and Gary is white then Gary is cold.
((("Gary" "is" "green" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "cold" "+"))
Quiet, cold people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Gary is not quiet.
False
1
inv-proof
[(triple8)]
("Gary" "is" "quiet" "-")
triple8
Erin is big.
True
2
proof
[(((triple5) -> rule4))]
("Erin" "is" "big" "+")
((triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple8) -> rule4))]
("Gary" "is" "big" "-")
((triple8) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Dave is green.
True
4
proof
[(((triple4 ((triple3) -> rule4)) -> rule6))]
("Dave" "is" "green" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule5) OR ((triple10 ((triple8) -> rule4)) -> rule6) OR ((((((triple8 triple7) -> rule8)) -> rule2)) -> rule5))]
("Gary" "is" "green" "-")
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple10 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple8 triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Dave is cold.
True
5
proof
[(((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple4 ((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3))]
("Dave" "is" "cold" "-")
((((triple4 ((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
True
7
proof
[(((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8))]
("Dave" "is" "round" "+")
((triple3 ((((triple4 ((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not round.
False
7
inv-proof
[(((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8))]
("Dave" "is" "round" "-")
((triple3 ((((triple4 ((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is white.
True
8
proof
[(((((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8)) -> rule2))]
("Dave" "is" "white" "+")
((((triple3 ((((triple4 ((triple3) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Dave is not white.
False
8
inv-proof
[(((((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8)) -> rule2))]
("Dave" "is" "white" "-")
((((triple3 ((((triple4 ((triple3) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "big" "+")
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is green.[(triple1)] Bob is white.[(triple2)] Dave is quiet.[(triple3)] Dave is smart.[(triple4)] Erin is quiet.[(triple5)] Erin is round.[(triple6)] Gary is cold.[(triple7 OR ((((((triple9) -> rule2)) -> rule5)) -> rule3) OR ((((triple10 ((triple8) -> rule4)) -> rule6)) -> rule3) OR ((((((triple9) -> rule2)) -> rule5) ((triple9) -> rule2)) -> rule7) OR ((((triple10 ((triple8) -> rule4)) -> rule6) ((triple9) -> rule2)) -> rule7))] Gary is quiet.[(triple8)] Gary is round.[(triple9 OR ((triple8 triple7) -> rule8) OR ((triple8 ((((triple10 ((triple8) -> rule4)) -> rule6)) -> rule3)) -> rule8))] Gary is smart.[(triple10 OR ((triple9 ((((triple9) -> rule2)) -> rule5)) -> rule1) OR ((((triple8 triple7) -> rule8) ((((triple9) -> rule2)) -> rule5)) -> rule1) OR ((triple9 ((((((triple8 triple7) -> rule8)) -> rule2)) -> rule5)) -> rule1) OR ((((triple8 triple7) -> rule8) ((((((triple8 triple7) -> rule8)) -> rule2)) -> rule5)) -> rule1))] @1: Bob is cold.[(((triple1) -> rule3))] Dave is big.[(((triple3) -> rule4))] Erin is big.[(((triple5) -> rule4))] Erin is white.[(((triple6) -> rule2))] Gary is big.[(((triple8) -> rule4))] Gary is white.[(((triple9) -> rule2) OR ((((triple8 triple7) -> rule8)) -> rule2) OR ((((triple8 ((((triple10 ((triple8) -> rule4)) -> rule6)) -> rule3)) -> rule8)) -> rule2))] @2: Dave is green.[(((triple4 ((triple3) -> rule4)) -> rule6))] Gary is green.[(((((triple9) -> rule2)) -> rule5) OR ((triple10 ((triple8) -> rule4)) -> rule6) OR ((((((triple8 triple7) -> rule8)) -> rule2)) -> rule5))] @3: Dave is cold.[(((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3))] @4: Dave is round.[(((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8))] @5: Dave is white.[(((((triple3 ((((triple4 ((triple3) -> rule4)) -> rule6)) -> rule3)) -> rule8)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((((((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple10 ((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple9) -> (rule2 % int3))) -> (rule5 % int2)) ((triple9) -> (rule2 % int3))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple10 ((triple8) -> (rule4 % int4))) -> (rule6 % int3)) ((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
((triple8 triple7) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple8 ((((triple10 ((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple9 ((((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple8 triple7) -> (rule8 % int4)) ((((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((triple9 ((((((triple8 triple7) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((((triple8 triple7) -> (rule8 % int4)) ((((((triple8 triple7) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple8) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple9) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple8 triple7) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple8 ((((triple10 ((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Dave is green.
("Dave" "is" "green" "+")
((triple4 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple10 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple8 triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((triple4 ((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((triple3 ((((triple4 ((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((triple3 ((((triple4 ((triple3) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5