Anne is nice. Dave is big. Harry is quiet. If something is big and not nice then it is red. If something is nice and round then it is red. All nice things are cold. If something is nice then it is round. If something is cold and not red then it is young. All red things are young. All young things are quiet. If something is young and big then it is quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is big and not nice then it is red.
((("something" "is" "big" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
If something is nice and round then it is red.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is cold and not red then it is young.
((("something" "is" "cold" "+") ("something" "is" "red" "~")) -> ("something" "is" "young" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is young and big then it is quiet.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("Anne" "is" "red" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "young" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Dave is big.[(triple2)] Harry is quiet.[(triple3)] @1: Anne is cold.[(((triple1) -> rule3))] Anne is round.[(((triple1) -> rule4))] @2: Anne is red.[(((triple1 ((triple1) -> rule4)) -> rule2))] @3: Anne is young.[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule6))] @4: Anne is quiet.[(((((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule6)) -> rule7))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1 ((triple1) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4