Anne is white. Charlie is big. Charlie is furry. Charlie is quiet. Charlie is smart. Dave is big. Dave is smart. Gary is cold. Gary is round. Gary is white. If Gary is smart then Gary is furry. All cold people are quiet. If someone is quiet then they are smart. If Charlie is big and Charlie is white then Charlie is cold. If someone is smart and big then they are round. If someone is white and big then they are cold. If someone is round then they are cold. If Dave is furry and Dave is cold then Dave is quiet.
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is smart then Gary is furry.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "furry" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is big and Charlie is white then Charlie is cold.
((("Charlie" "is" "big" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is smart and big then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is white and big then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If Dave is furry and Dave is cold then Dave is quiet.
((("Dave" "is" "furry" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "-")
triple9
Dave is round.
True
3
proof
[(((triple7 triple6) -> rule5))]
("Dave" "is" "round" "+")
((triple7 triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple7 triple6) -> rule5))]
("Dave" "is" "round" "-")
((triple7 triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
True
4
proof
[(((((triple7 triple6) -> rule5)) -> rule7))]
("Dave" "is" "cold" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule3) OR ((((((triple9) -> rule7)) -> rule2)) -> rule3))]
("Gary" "is" "smart" "-")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Dave is quiet.
True
5
proof
[(((((((triple7 triple6) -> rule5)) -> rule7)) -> rule2))]
("Dave" "is" "quiet" "+")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule3)) -> rule1) OR ((((((((triple9) -> rule7)) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "furry" "-")
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((((triple9) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not quiet.
Unknown
inv-rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule5 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is smart.
Unknown
rconc
[@4: Anne is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule7 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is white.[(triple1)] Charlie is big.[(triple2)] Charlie is furry.[(triple3)] Charlie is quiet.[(triple4 OR ((((((triple5 triple2) -> rule5)) -> rule7)) -> rule2))] Charlie is smart.[(triple5 OR ((triple4) -> rule3))] Dave is big.[(triple6)] Dave is smart.[(triple7)] Gary is cold.[(triple8 OR ((triple9) -> rule7))] Gary is round.[(triple9)] Gary is white.[(triple10)] @1: Charlie is round.[(((triple5 triple2) -> rule5) OR ((((triple4) -> rule3) triple2) -> rule5))] Dave is round.[(((triple7 triple6) -> rule5))] Gary is quiet.[(((triple8) -> rule2) OR ((((triple9) -> rule7)) -> rule2))] @2: Charlie is cold.[(((((triple5 triple2) -> rule5)) -> rule7) OR ((((((triple4) -> rule3) triple2) -> rule5)) -> rule7))] Dave is cold.[(((((triple7 triple6) -> rule5)) -> rule7))] Gary is smart.[(((((triple8) -> rule2)) -> rule3) OR ((((((triple9) -> rule7)) -> rule2)) -> rule3))] @3: Dave is quiet.[(((((((triple7 triple6) -> rule5)) -> rule7)) -> rule2))] Gary is furry.[(((((((triple8) -> rule2)) -> rule3)) -> rule1) OR ((((((((triple9) -> rule7)) -> rule2)) -> rule3)) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((((((triple5 triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple9) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
((triple5 triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple7 triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple5 triple2) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple4) -> (rule3 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((((triple9) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4