Anne is big. Anne is quiet. Charlie is big. Charlie is quiet. Charlie is round. Dave is big. Dave is green. Dave is nice. Dave is red. Dave is round. Harry is green. Harry is kind. Harry is quiet. Harry is red. Harry is round. If Anne is round and Anne is nice then Anne is kind. If Anne is big and Anne is green then Anne is red. If someone is round then they are quiet. Quiet people are green. If Charlie is round then Charlie is red. If someone is green then they are nice. Round, nice people are green. All green people are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Anne is round and Anne is nice then Anne is kind.
((("Anne" "is" "round" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
If Anne is big and Anne is green then Anne is red.
((("Anne" "is" "big" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "red" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Charlie is round then Charlie is red.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Round, nice people are green.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Charlie is quiet.
True
1
proof
[(triple4 OR ((triple5) -> rule3))]
("Charlie" "is" "quiet" "+")
triple4
((triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Charlie is red.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "red" "+")
((triple5) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple5) -> rule3)) -> rule4))]
("Charlie" "is" "green" "-")
((triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is quiet.[(triple2)] Charlie is big.[(triple3)] Charlie is quiet.[(triple4 OR ((triple5) -> rule3))] Charlie is round.[(triple5)] Dave is big.[(triple6)] Dave is green.[(triple7 OR ((triple10 triple8) -> rule7) OR ((((triple10) -> rule3)) -> rule4))] Dave is nice.[(triple8 OR ((triple7) -> rule6) OR ((triple7) -> rule8) OR ((((((triple10) -> rule3)) -> rule4)) -> rule6) OR ((((((triple10) -> rule3)) -> rule4)) -> rule8))] Dave is red.[(triple9)] Dave is round.[(triple10)] Harry is green.[(triple11 OR ((triple13) -> rule4) OR ((((triple15) -> rule3)) -> rule4))] Harry is kind.[(triple12)] Harry is quiet.[(triple13 OR ((triple15) -> rule3))] Harry is red.[(triple14)] Harry is round.[(triple15)] @1: Anne is green.[(((triple2) -> rule4))] Charlie is green.[(((triple4) -> rule4) OR ((((triple5) -> rule3)) -> rule4))] Charlie is red.[(((triple5) -> rule5))] Dave is quiet.[(((triple10) -> rule3))] Harry is nice.[(((triple11) -> rule6) OR ((triple11) -> rule8) OR ((((triple13) -> rule4)) -> rule6) OR ((((triple13) -> rule4)) -> rule8) OR ((((((triple15) -> rule3)) -> rule4)) -> rule6) OR ((((((triple15) -> rule3)) -> rule4)) -> rule8))] @2: Anne is nice.[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule4)) -> rule8))] Anne is red.[(((triple1 ((triple2) -> rule4)) -> rule2))] Charlie is nice.[(((((triple4) -> rule4)) -> rule6) OR ((((triple4) -> rule4)) -> rule8) OR ((((((triple5) -> rule3)) -> rule4)) -> rule6) OR ((((((triple5) -> rule3)) -> rule4)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple10 triple8) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple7) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
((triple13) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple15) -> (rule3 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple10) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple11) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple11) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple13) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple15) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple15) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3