Anne is quiet. Anne is white. Anne is young. Charlie is not green. Charlie is not rough. Charlie is young. Dave is green. Dave is quiet. Dave is rough. Gary is quiet. Gary is red. Gary is rough. If someone is quiet and young then they are furry. If someone is white then they are young. All rough people are white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is quiet and young then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is white then they are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Gary is quiet.
True
1
proof
[(triple10)]
("Gary" "is" "quiet" "+")
triple10
Dave is not green.
False
1
inv-proof
[(triple7)]
("Dave" "is" "green" "-")
triple7
Gary is white.
True
2
proof
[(((triple12) -> rule3))]
("Gary" "is" "white" "+")
((triple12) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is not furry.
False
3
inv-proof
[(((triple1 triple3) -> rule1) OR ((triple1 ((triple2) -> rule2)) -> rule1))]
("Anne" "is" "furry" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is young.
True
3
proof
[(((((triple9) -> rule3)) -> rule2))]
("Dave" "is" "young" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule2))]
("Gary" "is" "young" "-")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is furry.
True
5
proof
[(((triple8 ((((triple9) -> rule3)) -> rule2)) -> rule1))]
("Dave" "is" "furry" "+")
((triple8 ((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not furry.
False
5
inv-proof
[(((triple8 ((((triple9) -> rule3)) -> rule2)) -> rule1))]
("Dave" "is" "furry" "-")
((triple8 ((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Anne is young.[(triple3 OR ((triple2) -> rule2))] Charlie is not green.[(triple4)] Charlie is not rough.[(triple5)] Charlie is young.[(triple6)] Dave is green.[(triple7)] Dave is quiet.[(triple8)] Dave is rough.[(triple9)] Gary is quiet.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] @1: Anne is furry.[(((triple1 triple3) -> rule1) OR ((triple1 ((triple2) -> rule2)) -> rule1))] Dave is white.[(((triple9) -> rule3))] Gary is white.[(((triple12) -> rule3))] @2: Dave is young.[(((((triple9) -> rule3)) -> rule2))] Gary is young.[(((((triple12) -> rule3)) -> rule2))] @3: Dave is furry.[(((triple8 ((((triple9) -> rule3)) -> rule2)) -> rule1))] Gary is furry.[(((triple10 ((((triple12) -> rule3)) -> rule2)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is not green.
("Charlie" "is" "green" "-")
triple4
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple9) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple12) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple8 ((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((triple10 ((((triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3