Anne is big. Anne is green. Charlie is cold. Charlie is quiet. Dave is big. Dave is furry. Dave is young. If Charlie is cold then Charlie is rough. Furry people are young. Big people are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
If Charlie is cold then Charlie is rough.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "rough" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Anne is green.
True
1
proof
[(triple2)]
("Anne" "is" "green" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Charlie is rough.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Charlie is cold.[(triple3)] Charlie is quiet.[(triple4)] Dave is big.[(triple5)] Dave is furry.[(triple6 OR ((triple5) -> rule3))] Dave is young.[(triple7 OR ((triple6) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] @1: Anne is furry.[(((triple1) -> rule3))] Charlie is rough.[(((triple3) -> rule1))] @2: Anne is young.[(((((triple1) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2