Dave is big. Erin is kind. Erin is rough. If someone is furry and rough then they are young. If Dave is big then Dave is kind. If Dave is big then Dave is young. All kind people are furry. All kind people are not nice. Smart, rough people are nice. If Dave is not young then Dave is nice. If Dave is not rough then Dave is nice.
Dave is big.
("Dave" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If someone is furry and rough then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Dave is big then Dave is kind.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If Dave is big then Dave is young.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "young" "+"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All kind people are not nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
Smart, rough people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not young then Dave is nice.
((("Dave" "is" "young" "~")) -> ("Dave" "is" "nice" "+"))
If Dave is not rough then Dave is nice.
((("Dave" "is" "rough" "~")) -> ("Dave" "is" "nice" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "young" "+")
((triple1) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
True
4
proof
[(((((triple2) -> rule4) triple3) -> rule1))]
("Erin" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Dave is big.[(triple1)] Erin is kind.[(triple2)] Erin is rough.[(triple3)] @1: Dave is kind.[(((triple1) -> rule2))] Dave is young.[(((triple1) -> rule3))] Erin is furry.[(((triple2) -> rule4))] Erin is not nice.[(((triple2) -> rule5))] @2: Dave is furry.[(((((triple1) -> rule2)) -> rule4))] Dave is not nice.[(((((triple1) -> rule2)) -> rule5))] Erin is young.[(((((triple2) -> rule4) triple3) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2