Anne is red. Dave is kind. Harry is kind. All kind, blue people are white. Big people are nice. If Anne is blue then Anne is big. All blue people are big. Kind people are blue. All big people are blue. White people are big. All red people are kind.
Anne is red.
("Anne" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind, blue people are white.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If Anne is blue then Anne is big.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Harry is not kind.
False
1
inv-proof
[(triple3)]
("Harry" "is" "kind" "-")
triple3
Dave is blue.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "blue" "-")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is red.[(triple1)] Dave is kind.[(triple2)] Harry is kind.[(triple3)] @1: Anne is kind.[(((triple1) -> rule8))] Dave is blue.[(((triple2) -> rule5))] Harry is blue.[(((triple3) -> rule5))] @2: Anne is blue.[(((((triple1) -> rule8)) -> rule5))] Dave is big.[(((((triple2) -> rule5)) -> rule4) OR ((((triple2 ((triple2) -> rule5)) -> rule1)) -> rule7))] Dave is white.[(((triple2 ((triple2) -> rule5)) -> rule1))] Harry is big.[(((((triple3) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule5)) -> rule1)) -> rule7))] Harry is white.[(((triple3 ((triple3) -> rule5)) -> rule1))] @3: Anne is big.[(((((((triple1) -> rule8)) -> rule5)) -> rule3) OR ((((((triple1) -> rule8)) -> rule5)) -> rule4) OR ((((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule5)) -> rule1)) -> rule7))] Anne is white.[(((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule5)) -> rule1))] Dave is nice.[(((((((triple2) -> rule5)) -> rule4)) -> rule2) OR ((((((triple2 ((triple2) -> rule5)) -> rule1)) -> rule7)) -> rule2))] Harry is nice.[(((((((triple3) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3 ((triple3) -> rule5)) -> rule1)) -> rule7)) -> rule2))] @4: Anne is nice.[(((((((((triple1) -> rule8)) -> rule5)) -> rule3)) -> rule2) OR ((((((((triple1) -> rule8)) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule5)) -> rule1)) -> rule7)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int4)) ((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple2 ((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((((triple1) -> (rule8 % int5)) ((((triple1) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5