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