Anne is cold. Charlie is smart. Fiona is red. All big, cold things are red. If something is cold then it is big. If Anne is smart then Anne is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All big, cold things are red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Anne is smart then Anne is cold.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "cold" "+"))
Charlie is smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Charlie is smart.[(triple2)] Fiona is red.[(triple3)] @1: Anne is big.[(((triple1) -> rule2))] @2: Anne is red.[(((((triple1) -> rule2) triple1) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2