Dave is big. Dave is green. Dave is nice. Dave is young. Erin is big. Erin is cold. Erin is young. If Erin is green then Erin is young. If Erin is young and Erin is cold then Erin is nice. All nice, cold things are big. White, green things are rough. All big, cold things are rough. If something is rough then it is nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is green then Erin is young.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "young" "+"))
If Erin is young and Erin is cold then Erin is nice.
((("Erin" "is" "young" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "nice" "+"))
All nice, cold things are big.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
White, green things are rough.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All big, cold things are rough.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Erin is big.
True
1
proof
[(triple5 OR ((((triple7 triple6) -> rule2) triple6) -> rule3))]
("Erin" "is" "big" "+")
triple5
((((triple7 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not cold.
False
1
inv-proof
[(triple6)]
("Erin" "is" "cold" "-")
triple6
Erin is nice.
True
3
proof
[(((triple7 triple6) -> rule2) OR ((((triple5 triple6) -> rule5)) -> rule6))]
("Erin" "is" "nice" "+")
((triple7 triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((triple5 triple6) -> rule5) OR ((((((triple7 triple6) -> rule2) triple6) -> rule3) triple6) -> rule5))]
("Erin" "is" "rough" "-")
((triple5 triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((((triple7 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Dave is big.[(triple1)] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is young.[(triple4)] Erin is big.[(triple5 OR ((((triple7 triple6) -> rule2) triple6) -> rule3))] Erin is cold.[(triple6)] Erin is young.[(triple7)] @1: Erin is nice.[(((triple7 triple6) -> rule2) OR ((((triple5 triple6) -> rule5)) -> rule6))] Erin is rough.[(((triple5 triple6) -> rule5) OR ((((((triple7 triple6) -> rule2) triple6) -> rule3) triple6) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((((triple7 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
((triple7 triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple5 triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((((triple7 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3