Anne is big. Anne is rough. Anne is smart. Charlie is cold. Charlie is red. Gary is rough. Harry is big. If someone is smart then they are blue. Quiet, cold people are not blue. If someone is smart and not quiet then they are big. Quiet, blue people are big. All red people are rough. Rough, red people are cold. If someone is quiet then they are cold. All quiet people are not cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Quiet, cold people are not blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "-"))
If someone is smart and not quiet then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "+"))
Quiet, blue people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Rough, red people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are not cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "-"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple4 OR ((((triple5) -> rule5) triple5) -> rule6))]
("Charlie" "is" "cold" "-")
triple4
((((triple5) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is rough.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple5) -> rule5))]
("Charlie" "is" "rough" "-")
((triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3)] Charlie is cold.[(triple4 OR ((((triple5) -> rule5) triple5) -> rule6))] Charlie is red.[(triple5)] Gary is rough.[(triple6)] Harry is big.[(triple7)] @1: Anne is blue.[(((triple3) -> rule1))] Charlie is rough.[(((triple5) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((((triple5) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1