Anne is cold. Anne is red. Bob is red. Bob is rough. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is red. Charlie is rough. Dave is cold. Dave is furry. Dave is nice. Dave is red. Dave is white. Dave is young. If something is nice then it is rough. All red things are nice.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Dave is furry.
True
1
proof
[(triple11)]
("Dave" "is" "furry" "+")
triple11
Charlie is not rough.
False
1
inv-proof
[(triple9 OR ((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
("Charlie" "is" "rough" "-")
triple9
((triple7) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is rough.
True
2
proof
[(((triple12) -> rule1) OR ((((triple13) -> rule2)) -> rule1))]
("Dave" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Anne is rough.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Anne" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Anne" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4 OR ((((triple3) -> rule2)) -> rule1))] Charlie is cold.[(triple5)] Charlie is furry.[(triple6)] Charlie is nice.[(triple7 OR ((triple8) -> rule2))] Charlie is red.[(triple8)] Charlie is rough.[(triple9 OR ((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Dave is cold.[(triple10)] Dave is furry.[(triple11)] Dave is nice.[(triple12 OR ((triple13) -> rule2))] Dave is red.[(triple13)] Dave is white.[(triple14)] Dave is young.[(triple15)] @1: Anne is nice.[(((triple2) -> rule2))] Bob is nice.[(((triple3) -> rule2))] Dave is rough.[(((triple12) -> rule1) OR ((((triple13) -> rule2)) -> rule1))] @2: Anne is rough.[(((((triple2) -> rule2)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
((triple7) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple10
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple13) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple14
Dave is young.
("Dave" "is" "young" "+")
triple15
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2