Dave is blue. Dave is green. Dave is kind. Gary is blue. Harry is kind. Harry is red. Harry is round. If something is young and big then it is red. If something is green and kind then it is red. All red, round things are green. If something is young then it is blue. Green, red things are young. All green, round things are young.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is young and big then it is red.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is green and kind then it is red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All red, round things are green.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Green, red things are young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All green, round things are young.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Harry is green.
True
3
proof
[(((triple6 triple7) -> rule3))]
("Harry" "is" "green" "+")
((triple6 triple7) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("Dave" "is" "red" "-")
((triple2 triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is young.
True
5
proof
[(((((triple6 triple7) -> rule3) triple6) -> rule5) OR ((((triple6 triple7) -> rule3) triple7) -> rule6))]
("Harry" "is" "young" "+")
((((triple6 triple7) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not young.
False
5
inv-proof
[(((((triple6 triple7) -> rule3) triple6) -> rule5) OR ((((triple6 triple7) -> rule3) triple7) -> rule6))]
("Harry" "is" "young" "-")
((((triple6 triple7) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
True
6
proof
[(((((((triple6 triple7) -> rule3) triple6) -> rule5)) -> rule4) OR ((((((triple6 triple7) -> rule3) triple7) -> rule6)) -> rule4))]
("Harry" "is" "blue" "+")
((((((triple6 triple7) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not blue.
False
6
inv-proof
[(((((((triple6 triple7) -> rule3) triple6) -> rule5)) -> rule4) OR ((((((triple6 triple7) -> rule3) triple7) -> rule6)) -> rule4))]
("Harry" "is" "blue" "-")
((((((triple6 triple7) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is blue.[(triple1 OR ((((triple2 ((triple2 triple3) -> rule2)) -> rule5)) -> rule4))] Dave is green.[(triple2)] Dave is kind.[(triple3)] Gary is blue.[(triple4)] Harry is kind.[(triple5)] Harry is red.[(triple6)] Harry is round.[(triple7)] @1: Dave is red.[(((triple2 triple3) -> rule2))] Harry is green.[(((triple6 triple7) -> rule3))] @2: Dave is young.[(((triple2 ((triple2 triple3) -> rule2)) -> rule5))] Harry is young.[(((((triple6 triple7) -> rule3) triple6) -> rule5) OR ((((triple6 triple7) -> rule3) triple7) -> rule6))] @3: Harry is blue.[(((((((triple6 triple7) -> rule3) triple6) -> rule5)) -> rule4) OR ((((((triple6 triple7) -> rule3) triple7) -> rule6)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((((triple2 ((triple2 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
((triple2 triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple6 triple7) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple2 ((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple6 triple7) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple6 triple7) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple6 triple7) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple6 triple7) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3