Anne is nice. Anne is red. Anne is round. Charlie is round. Charlie is young. Fiona is young. Gary is cold. Gary is rough. Gary is round. Gary is young. If someone is young and not cold then they are not red. Round people are young. All nice people are not white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is young and not cold then they are not red.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "-"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All nice people are not white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "-"))
Anne is round.
True
1
proof
[(triple3)]
("Anne" "is" "round" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple10 OR ((triple9) -> rule2))]
("Gary" "is" "young" "-")
triple10
((triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is not white.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3)] Charlie is round.[(triple4)] Charlie is young.[(triple5 OR ((triple4) -> rule2))] Fiona is young.[(triple6)] Gary is cold.[(triple7)] Gary is rough.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10 OR ((triple9) -> rule2))] @1: Anne is not white.[(((triple1) -> rule3))] Anne is young.[(((triple3) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1