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