Dave is big. Dave is blue. Dave is green. Erin is blue. Erin is furry. Erin is green. Erin is rough. All blue things are young. If something is green and rough then it is blue. Young things are rough.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is green and rough then it is blue.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Erin is green.
True
1
proof
[(triple6)]
("Erin" "is" "green" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is young.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple6 triple7) -> rule2)) -> rule1))]
("Erin" "is" "young" "-")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is green.[(triple3)] Erin is blue.[(triple4 OR ((triple6 triple7) -> rule2))] Erin is furry.[(triple5)] Erin is green.[(triple6)] Erin is rough.[(triple7 OR ((((triple4) -> rule1)) -> rule3))] @1: Dave is young.[(((triple2) -> rule1))] Erin is young.[(((triple4) -> rule1) OR ((((triple6 triple7) -> rule2)) -> rule1))] @2: Dave is rough.[(((((triple2) -> rule1)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
((triple6 triple7) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2