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