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