Anne is big. Anne is cold. Anne is nice. Anne is round. Charlie is nice. Charlie is quiet. Dave is round. Round things are nice. If something is red and not round then it is nice. If Anne is round then Anne is red. All red, big things are rough. If something is big and not nice then it is quiet. If Anne is nice and Anne is quiet then Anne is cold. If Anne is nice then Anne is cold. If Dave is not quiet then Dave is not rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is red and not round then it is nice.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "+"))
If Anne is round then Anne is red.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "red" "+"))
All red, big things are rough.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is big and not nice then it is quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If Anne is nice and Anne is quiet then Anne is cold.
((("Anne" "is" "nice" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "cold" "+"))
If Anne is nice then Anne is cold.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "cold" "+"))
If Dave is not quiet then Dave is not rough.
((("Dave" "is" "quiet" "~")) -> ("Dave" "is" "rough" "-"))
Anne is cold.
True
1
proof
[(triple2 OR ((triple3) -> rule7) OR ((((triple4) -> rule1)) -> rule7))]
("Anne" "is" "cold" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is not nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "-")
triple5
Dave is nice.
True
2
proof
[(((triple7) -> rule1))]
("Dave" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple7) -> rule1))]
("Dave" "is" "nice" "-")
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is rough.
True
4
proof
[(((((triple4) -> rule3) triple1) -> rule4))]
("Anne" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple4) -> rule3) triple1) -> rule4))]
("Anne" "is" "rough" "-")
((((triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple3) -> rule7) OR ((((triple4) -> rule1)) -> rule7))] Anne is nice.[(triple3 OR ((triple4) -> rule1))] Anne is round.[(triple4)] Charlie is nice.[(triple5)] Charlie is quiet.[(triple6)] Dave is round.[(triple7)] @1: Anne is red.[(((triple4) -> rule3))] Dave is nice.[(((triple7) -> rule1))] @2: Anne is rough.[(((((triple4) -> rule3) triple1) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple4) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple4) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2