Anne is furry. Anne is quiet. Dave is big. Dave is nice. Dave is smart. Harry is smart. Harry is young. Big, quiet people are nice. All quiet people are nice. If someone is nice then they are big. Rough, smart people are big. If someone is young and smart then they are quiet. All nice, smart people are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Big, quiet people are nice.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Rough, smart people are big.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is young and smart then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All nice, smart people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple6)]
("Harry" "is" "smart" "-")
triple6
Harry is quiet.
True
3
proof
[(((triple7 triple6) -> rule5))]
("Harry" "is" "quiet" "+")
((triple7 triple6) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple4 triple5) -> rule6))]
("Dave" "is" "quiet" "-")
((triple4 triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is nice.
True
4
proof
[(((((triple7 triple6) -> rule5)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is big.
True
5
proof
[(((((((triple7 triple6) -> rule5)) -> rule2)) -> rule3))]
("Harry" "is" "big" "+")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((((triple7 triple6) -> rule5)) -> rule2)) -> rule3))]
("Harry" "is" "big" "-")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Dave is big.[(triple3 OR ((triple4) -> rule3))] Dave is nice.[(triple4)] Dave is smart.[(triple5)] Harry is smart.[(triple6)] Harry is young.[(triple7)] @1: Anne is nice.[(((triple2) -> rule2))] Dave is quiet.[(((triple4 triple5) -> rule6))] Harry is quiet.[(((triple7 triple6) -> rule5))] @2: Anne is big.[(((((triple2) -> rule2)) -> rule3))] Harry is nice.[(((((triple7 triple6) -> rule5)) -> rule2))] @3: Harry is big.[(((((((triple7 triple6) -> rule5)) -> rule2)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
((triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4 triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 triple6) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3