Anne is cold. Anne is furry. Anne is green. Anne is young. Charlie is green. Charlie is young. Dave is green. Dave is white. Dave is young. Gary is furry. Gary is white. Gary is young. If something is young then it is cold. If something is white and green then it is nice. If Anne is cold then Anne is white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is white and green then it is nice.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Anne is cold then Anne is white.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "white" "+"))
Gary is white.
True
1
proof
[(triple11)]
("Gary" "is" "white" "+")
triple11
Dave is not white.
False
1
inv-proof
[(triple8)]
("Dave" "is" "white" "-")
triple8
Charlie is cold.
True
2
proof
[(((triple6) -> rule1))]
("Charlie" "is" "cold" "+")
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
True
4
proof
[(((((triple1) -> rule3) triple3) -> rule2) OR ((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((triple1) -> rule3) triple3) -> rule2) OR ((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is cold.[(triple1 OR ((triple4) -> rule1))] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is young.[(triple4)] Charlie is green.[(triple5)] Charlie is young.[(triple6)] Dave is green.[(triple7)] Dave is white.[(triple8)] Dave is young.[(triple9)] Gary is furry.[(triple10)] Gary is white.[(triple11)] Gary is young.[(triple12)] @1: Anne is white.[(((triple1) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Charlie is cold.[(((triple6) -> rule1))] Dave is cold.[(((triple9) -> rule1))] Dave is nice.[(((triple8 triple7) -> rule2))] Gary is cold.[(((triple12) -> rule1))] @2: Anne is nice.[(((((triple1) -> rule3) triple3) -> rule2) OR ((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple9) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple8 triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3