Anne is red. Charlie is cold. Fiona is green. Gary is smart. If someone is red then they are rough. Big, cold people are smart. If someone is smart and not rough then they are green. If someone is cold then they are green. If someone is big and not green then they are quiet. All smart people are quiet.
Anne is red.
("Anne" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big, cold people are smart.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not rough then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "green" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not green then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "quiet" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Fiona is not green.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "green" "-")
triple3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is red.[(triple1)] Charlie is cold.[(triple2)] Fiona is green.[(triple3)] Gary is smart.[(triple4)] @1: Anne is rough.[(((triple1) -> rule1))] Charlie is green.[(((triple2) -> rule4))] Gary is quiet.[(((triple4) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1