Bob is furry. Bob is rough. Charlie is cold. Charlie is red. Dave is cold. Dave is quiet. Dave is red. Dave is rough. Fiona is red. Fiona is rough. All round, red people are rough. Red, round people are big. Red people are cold. Big people are red. All rough people are quiet. Round people are big. All quiet people are round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All round, red people are rough.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Red, round people are big.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Dave is red.
True
1
proof
[(triple7 OR ((((((triple6) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple8) -> rule5)) -> rule7)) -> rule6)) -> rule4))]
("Dave" "is" "red" "+")
triple7
((((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is not cold.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule3) OR ((((((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule3) OR ((((((((((triple8) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))]
("Dave" "is" "cold" "-")
triple5
((triple7) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((((triple8) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
Fiona is cold.
True
2
proof
[(((triple9) -> rule3) OR ((((((((((triple10) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))]
("Fiona" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((((((((triple10) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is big.
True
3
proof
[(((((triple6) -> rule7)) -> rule6) OR ((triple7 ((triple6) -> rule7)) -> rule2) OR ((((((triple8) -> rule5)) -> rule7)) -> rule6) OR ((triple7 ((((triple8) -> rule5)) -> rule7)) -> rule2))]
("Dave" "is" "big" "+")
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple7 ((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple7 ((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not big.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule6) OR ((triple7 ((triple6) -> rule7)) -> rule2) OR ((((((triple8) -> rule5)) -> rule7)) -> rule6) OR ((triple7 ((((triple8) -> rule5)) -> rule7)) -> rule2))]
("Dave" "is" "big" "-")
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple7 ((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple7 ((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Bob is big.
True
4
proof
[(((((((triple2) -> rule5)) -> rule7)) -> rule6))]
("Bob" "is" "big" "+")
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Fiona is not big.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule7)) -> rule6) OR ((triple9 ((((triple10) -> rule5)) -> rule7)) -> rule2))]
("Fiona" "is" "big" "-")
((((((triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple9 ((((triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Bob is red.
True
5
proof
[(((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4))]
("Bob" "is" "red" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not red.
False
5
inv-proof
[(((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4))]
("Bob" "is" "red" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is cold.
True
6
proof
[(((((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))]
("Bob" "is" "cold" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Bob is not cold.
False
6
inv-proof
[(((((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))]
("Bob" "is" "cold" "-")
((((((((((triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Charlie is not rough.
Unknown
inv-rconc
[@3: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@3: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule7 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is big.
Unknown
rconc
[@4: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is rough.[(triple2)] Charlie is cold.[(triple3 OR ((triple4) -> rule3))] Charlie is red.[(triple4)] Dave is cold.[(triple5 OR ((triple7) -> rule3) OR ((((((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule3) OR ((((((((((triple8) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))] Dave is quiet.[(triple6 OR ((triple8) -> rule5))] Dave is red.[(triple7 OR ((((((triple6) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple8) -> rule5)) -> rule7)) -> rule6)) -> rule4))] Dave is rough.[(triple8 OR ((((triple6) -> rule7) triple7) -> rule1) OR ((((triple6) -> rule7) ((((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule1))] Fiona is red.[(triple9 OR ((((((((triple10) -> rule5)) -> rule7)) -> rule6)) -> rule4))] Fiona is rough.[(triple10)] @1: Bob is quiet.[(((triple2) -> rule5))] Dave is round.[(((triple6) -> rule7) OR ((((triple8) -> rule5)) -> rule7))] Fiona is cold.[(((triple9) -> rule3) OR ((((((((((triple10) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))] Fiona is quiet.[(((triple10) -> rule5))] @2: Bob is round.[(((((triple2) -> rule5)) -> rule7))] Dave is big.[(((((triple6) -> rule7)) -> rule6) OR ((triple7 ((triple6) -> rule7)) -> rule2) OR ((((((triple8) -> rule5)) -> rule7)) -> rule6) OR ((triple7 ((((triple8) -> rule5)) -> rule7)) -> rule2))] Fiona is round.[(((((triple10) -> rule5)) -> rule7))] @3: Bob is big.[(((((((triple2) -> rule5)) -> rule7)) -> rule6))] Fiona is big.[(((((((triple10) -> rule5)) -> rule7)) -> rule6) OR ((triple9 ((((triple10) -> rule5)) -> rule7)) -> rule2))] @4: Bob is red.[(((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4))] @5: Bob is cold.[(((((((((((triple2) -> rule5)) -> rule7)) -> rule6)) -> rule4)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple4) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple7) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((((triple8) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((triple8) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple7
((((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple8
((((triple6) -> (rule7 % int2)) triple7) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6) -> (rule7 % int4)) ((((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
triple9
((((((((triple10) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((((((((triple10) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple7 ((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple7 ((((triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple9 ((((triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5