Dave is red. Erin is rough. All rough people are not big. If someone is young and green then they are not round. Big people are young. If Dave is not green then Dave is round. If someone is young then they are rough. Red people are rough. If Dave is not white then Dave is rough. Green people are red.
Dave is red.
("Dave" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All rough people are not big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "-"))
If someone is young and green then they are not round.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "-"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Dave is not green then Dave is round.
((("Dave" "is" "green" "~")) -> ("Dave" "is" "round" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Dave is not white then Dave is rough.
((("Dave" "is" "white" "~")) -> ("Dave" "is" "rough" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Dave is rough.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "big" "+")
((triple2) -> (rule1 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Dave is not big.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Dave" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Dave" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "red" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "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 red.[(triple1)] Erin is rough.[(triple2)] @1: Dave is rough.[(((triple1) -> rule6))] Erin is not big.[(((triple2) -> rule1))] @2: Dave is not big.[(((((triple1) -> rule6)) -> rule1))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
((triple2) -> (rule1 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Dave is not big.
("Dave" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2