Anne is cold. Anne is quiet. Bob is cold. Bob is quiet. Bob is red. Gary is cold. Gary is young. If Bob is rough then Bob is not furry. Cold things are rough. If something is smart and not rough then it is not quiet. All rough, red things are quiet. If Anne is cold and Anne is red then Anne is young. If something is quiet and not cold then it is not red. Cold, rough things are red. If something is red and not quiet then it is not young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
If Bob is rough then Bob is not furry.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "furry" "-"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is smart and not rough then it is not quiet.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "-"))
All rough, red things are quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Anne is cold and Anne is red then Anne is young.
((("Anne" "is" "cold" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "young" "+"))
If something is quiet and not cold then it is not red.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "-"))
Cold, rough things are red.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is red and not quiet then it is not young.
((("something" "is" "red" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple5 OR ((triple3 ((triple3) -> rule2)) -> rule7))]
("Bob" "is" "red" "-")
triple5
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is red.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule7))]
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Bob is furry.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is young.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule7)) -> rule5))]
("Anne" "is" "young" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not young.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule7)) -> rule5))]
("Anne" "is" "young" "-")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2 OR ((((triple1) -> rule2) ((triple1 ((triple1) -> rule2)) -> rule7)) -> rule4))] Bob is cold.[(triple3)] Bob is quiet.[(triple4 OR ((((triple3) -> rule2) triple5) -> rule4) OR ((((triple3) -> rule2) ((triple3 ((triple3) -> rule2)) -> rule7)) -> rule4))] Bob is red.[(triple5 OR ((triple3 ((triple3) -> rule2)) -> rule7))] Gary is cold.[(triple6)] Gary is young.[(triple7)] @1: Anne is rough.[(((triple1) -> rule2))] Bob is rough.[(((triple3) -> rule2))] Gary is rough.[(((triple6) -> rule2))] @2: Anne is red.[(((triple1 ((triple1) -> rule2)) -> rule7))] Bob is not furry.[(((((triple3) -> rule2)) -> rule1))] Gary is red.[(((triple6 ((triple6) -> rule2)) -> rule7))] @3: Anne is young.[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule7)) -> rule5))] Gary is quiet.[(((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule7)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((((triple1) -> (rule2 % int3)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((((triple3) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple6) -> (rule2 % int3)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3