Dave is young. Erin is red. Erin is young. Round people are rough. All young people are round. Nice people are rough. If someone is red then they are cold. Cold people are round. Red people are round.
Dave is young.
("Dave" "is" "young" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple1)]
("Dave" "is" "young" "-")
triple1
Erin is cold.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule6) OR ((triple3) -> rule2) OR ((((triple2) -> rule4)) -> rule5))]
("Erin" "is" "round" "-")
((triple2) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple3) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
True
3
proof
[(((((triple2) -> rule6)) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple2) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Dave is not rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is young.[(triple1)] Erin is red.[(triple2)] Erin is young.[(triple3)] @1: Dave is round.[(((triple1) -> rule2))] Erin is cold.[(((triple2) -> rule4))] Erin is round.[(((triple2) -> rule6) OR ((triple3) -> rule2) OR ((((triple2) -> rule4)) -> rule5))] @2: Dave is rough.[(((((triple1) -> rule2)) -> rule1))] Erin is rough.[(((((triple2) -> rule6)) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple2) -> rule4)) -> rule5)) -> rule1))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple3) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3