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