Dave is big. Erin is not kind. Harry is young. If Dave is rough then Dave is young. If something is big and not kind then it is quiet. Big, red things are rough. If something is big then it is red. All kind, red things are furry. If something is quiet and not young then it is not furry.
Dave is big.
("Dave" "is" "big" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Harry is young.
("Harry" "is" "young" "+")
If Dave is rough then Dave is young.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "young" "+"))
If something is big and not kind then it is quiet.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
Big, red things are rough.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind, red things are furry.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is quiet and not young then it is not furry.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "-"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Dave is red.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "red" "+")
((triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "red" "-")
((triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Dave" "is" "rough" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Dave" "is" "rough" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is young.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule3)) -> rule1))]
("Dave" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule3)) -> rule1))]
("Dave" "is" "young" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Dave is big.[(triple1)] Erin is not kind.[(triple2)] Harry is young.[(triple3)] @1: Dave is red.[(((triple1) -> rule4))] @2: Dave is rough.[(((triple1 ((triple1) -> rule4)) -> rule3))] @3: Dave is young.[(((((triple1 ((triple1) -> rule4)) -> rule3)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Erin is not kind.
("Erin" "is" "kind" "-")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3