Anne is red. Charlie is blue. Charlie is green. Charlie is quiet. Charlie is smart. Fiona is blue. Fiona is young. If something is blue and not smart then it is cold. All young, smart things are not blue. If something is young then it is green. If something is blue and not cold then it is not green. If something is green and not cold then it is not red. If something is smart then it is red.
Anne is red.
("Anne" "is" "red" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is blue and not smart then it is cold.
((("something" "is" "blue" "+") ("something" "is" "smart" "~")) -> ("something" "is" "cold" "+"))
All young, smart things are not blue.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "-"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is blue and not cold then it is not green.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "-"))
If something is green and not cold then it is not red.
((("something" "is" "green" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "-"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Charlie is smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "+")
triple5
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Fiona is green.
True
2
proof
[(((triple7) -> rule3))]
("Fiona" "is" "green" "+")
((triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple5) -> rule6))]
("Charlie" "is" "red" "-")
((triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is red.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3)] Charlie is quiet.[(triple4)] Charlie is smart.[(triple5)] Fiona is blue.[(triple6)] Fiona is young.[(triple7)] @1: Charlie is red.[(((triple5) -> rule6))] Fiona is green.[(((triple7) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1