Dave is big. Dave is quiet. Erin is white. White people are big. All rough, cold people are nice. Young people are quiet. If Dave is big then Dave is rough. All rough, quiet people are young. If someone is cold then they are rough. Quiet people are rough. If Erin is big then Erin is white.
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All rough, cold people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is big then Dave is rough.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "rough" "+"))
All rough, quiet people are young.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Erin is big then Erin is white.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "white" "+"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Erin is big.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "big" "+")
((triple3) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple2) -> rule7))]
("Dave" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple2) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
True
4
proof
[(((((triple1) -> rule4) triple2) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule5))]
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple1) -> rule4) triple2) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule5))]
("Dave" "is" "young" "-")
((((triple1) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not young.
Unknown
inv-rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "young" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is big.[(triple1)] Dave is quiet.[(triple2)] Erin is white.[(triple3)] @1: Dave is rough.[(((triple1) -> rule4) OR ((triple2) -> rule7))] Erin is big.[(((triple3) -> rule1))] @2: Dave is young.[(((((triple1) -> rule4) triple2) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple2) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2