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