Anne is green. Charlie is green. Dave is green. Harry is red. If Charlie is green then Charlie is kind. Green, young people are red. Red people are blue. If someone is rough and big then they are green. All red, rough people are kind. Kind people are young. If Charlie is rough then Charlie is young. Blue, kind people are green.
Anne is green.
("Anne" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
If Charlie is green then Charlie is kind.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "kind" "+"))
Green, young people are red.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and big then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All red, rough people are kind.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Charlie is rough then Charlie is young.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
Blue, kind people are green.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Harry is red.
True
1
proof
[(triple4)]
("Harry" "is" "red" "+")
triple4
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
True
5
proof
[(((triple2 ((((triple2) -> rule1)) -> rule6)) -> rule2))]
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule1)) -> rule6)) -> rule2))]
("Charlie" "is" "red" "-")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is red.
Unknown
rconc
[@3: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule5 <- FAIL)]]
("Anne" "is" "red" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is green.[(triple1)] Charlie is green.[(triple2)] Dave is green.[(triple3)] Harry is red.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule1))] Harry is blue.[(((triple4) -> rule3))] @2: Charlie is young.[(((((triple2) -> rule1)) -> rule6))] @3: Charlie is red.[(((triple2 ((((triple2) -> rule1)) -> rule6)) -> rule2))] @4: Charlie is blue.[(((((triple2 ((((triple2) -> rule1)) -> rule6)) -> rule2)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4