Anne is furry. Anne is kind. Anne is nice. Charlie is quiet. Charlie is red. Charlie is smart. Harry is big. Harry is furry. Harry is kind. Harry is quiet. If Anne is nice then Anne is kind. If someone is furry then they are big. Furry people are smart. All red people are furry. All nice, kind people are furry. Furry, kind people are big. All smart people are red. Kind, red people are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Anne is nice then Anne is kind.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All nice, kind people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Furry, kind people are big.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Kind, red people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Harry is quiet.
True
1
proof
[(triple10 OR ((triple9 ((((triple8) -> rule3)) -> rule7)) -> rule8))]
("Harry" "is" "quiet" "+")
triple10
((triple9 ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not big.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule2) OR ((triple8 triple9) -> rule6))]
("Harry" "is" "big" "-")
triple7
((triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is smart.
True
2
proof
[(((triple1) -> rule3) OR ((((triple3 triple2) -> rule5)) -> rule3) OR ((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple3 triple2) -> rule5)) -> rule3) OR ((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is furry.[(triple1 OR ((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule1)) -> rule5))] Anne is kind.[(triple2 OR ((triple3) -> rule1))] Anne is nice.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5 OR ((triple6) -> rule7))] Charlie is smart.[(triple6 OR ((((triple5) -> rule4)) -> rule3))] Harry is big.[(triple7 OR ((triple8) -> rule2) OR ((triple8 triple9) -> rule6))] Harry is furry.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10 OR ((triple9 ((((triple8) -> rule3)) -> rule7)) -> rule8))] @1: Anne is big.[(((triple1) -> rule2) OR ((triple1 triple2) -> rule6) OR ((((triple3 triple2) -> rule5)) -> rule2) OR ((triple1 ((triple3) -> rule1)) -> rule6) OR ((((triple3 triple2) -> rule5) triple2) -> rule6) OR ((((triple3 triple2) -> rule5) ((triple3) -> rule1)) -> rule6) OR ((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule2) OR ((((triple3 ((triple3) -> rule1)) -> rule5) triple2) -> rule6) OR ((((triple3 ((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule6))] Anne is smart.[(((triple1) -> rule3) OR ((((triple3 triple2) -> rule5)) -> rule3) OR ((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3))] Charlie is furry.[(((triple5) -> rule4) OR ((((triple6) -> rule7)) -> rule4))] Harry is smart.[(((triple8) -> rule3))] @2: Anne is red.[(((((triple1) -> rule3)) -> rule7) OR ((((((triple3 triple2) -> rule5)) -> rule3)) -> rule7) OR ((((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3)) -> rule7))] Charlie is big.[(((((triple5) -> rule4)) -> rule2) OR ((((((triple6) -> rule7)) -> rule4)) -> rule2))] Harry is red.[(((((triple8) -> rule3)) -> rule7))] @3: Anne is quiet.[(((triple2 ((((triple1) -> rule3)) -> rule7)) -> rule8) OR ((((triple3) -> rule1) ((((triple1) -> rule3)) -> rule7)) -> rule8) OR ((triple2 ((((((triple3 triple2) -> rule5)) -> rule3)) -> rule7)) -> rule8) OR ((((triple3) -> rule1) ((((((triple3 triple2) -> rule5)) -> rule3)) -> rule7)) -> rule8) OR ((triple2 ((((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3)) -> rule7)) -> rule8) OR ((((triple3) -> rule1) ((((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule3)) -> rule7)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple3 triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple6) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple9 ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple1 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple3 triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 triple2) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple3 triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple3 ((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple3) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((triple2 ((((((triple3 triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
((((triple3) -> (rule1 % int5)) ((((((triple3 triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5
((triple2 ((((((triple3 ((triple3) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5
((((triple3) -> (rule1 % int5)) ((((((triple3 ((triple3) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5