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