Charlie is furry. Charlie is round. Erin is furry. Erin is quiet. Gary is big. Gary is nice. Gary is quiet. Gary is red. Gary is smart. Harry is quiet. If something is nice and smart then it is quiet. If Erin is red and Erin is round then Erin is nice. If Erin is nice and Erin is furry then Erin is quiet. Smart, big things are furry. Nice things are big. All red things are quiet. If something is red then it is smart. If Harry is smart and Harry is nice then Harry is furry.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is nice and smart then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Erin is red and Erin is round then Erin is nice.
((("Erin" "is" "red" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "nice" "+"))
If Erin is nice and Erin is furry then Erin is quiet.
((("Erin" "is" "nice" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "quiet" "+"))
Smart, big things are furry.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Harry is smart and Harry is nice then Harry is furry.
((("Harry" "is" "smart" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "+"))
Gary is quiet.
True
1
proof
[(triple7 OR ((triple8) -> rule6) OR ((triple6 triple9) -> rule1) OR ((triple6 ((triple8) -> rule7)) -> rule1))]
("Gary" "is" "quiet" "+")
triple7
((triple8) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple6 triple9) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple6 ((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Gary is furry.
True
3
proof
[(((triple9 triple5) -> rule4) OR ((triple9 ((triple6) -> rule5)) -> rule4) OR ((((triple8) -> rule7) triple5) -> rule4) OR ((((triple8) -> rule7) ((triple6) -> rule5)) -> rule4))]
("Gary" "is" "furry" "+")
((triple9 triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple9 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple8) -> (rule7 % int2)) triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not furry.
False
3
inv-proof
[(((triple9 triple5) -> rule4) OR ((triple9 ((triple6) -> rule5)) -> rule4) OR ((((triple8) -> rule7) triple5) -> rule4) OR ((((triple8) -> rule7) ((triple6) -> rule5)) -> rule4))]
("Gary" "is" "furry" "-")
((triple9 triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple9 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple8) -> (rule7 % int2)) triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Charlie is furry.[(triple1)] Charlie is round.[(triple2)] Erin is furry.[(triple3)] Erin is quiet.[(triple4)] Gary is big.[(triple5 OR ((triple6) -> rule5))] Gary is nice.[(triple6)] Gary is quiet.[(triple7 OR ((triple8) -> rule6) OR ((triple6 triple9) -> rule1) OR ((triple6 ((triple8) -> rule7)) -> rule1))] Gary is red.[(triple8)] Gary is smart.[(triple9 OR ((triple8) -> rule7))] Harry is quiet.[(triple10)] @1: Gary is furry.[(((triple9 triple5) -> rule4) OR ((triple9 ((triple6) -> rule5)) -> rule4) OR ((((triple8) -> rule7) triple5) -> rule4) OR ((((triple8) -> rule7) ((triple6) -> rule5)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple6) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
((triple8) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple6 triple9) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple6 ((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple8) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
((triple9 triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple9 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple8) -> (rule7 % int2)) triple5) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3