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