Anne is red. Bob is not nice. Erin is nice. If someone is rough then they are round. If someone is nice then they are round. Young people are green. Nice people are green. If someone is nice and not round then they are green. Round people are young. Round, green people are young. If Erin is young and Erin is not nice then Erin is red.
Anne is red.
("Anne" "is" "red" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not round then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "green" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Round, green people are young.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Erin is young and Erin is not nice then Erin is red.
((("Erin" "is" "young" "+") ("Erin" "is" "nice" "~")) -> ("Erin" "is" "red" "+"))
Bob is not nice.
True
1
proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Bob is nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Erin is round.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "round" "+")
((triple3) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((((triple3) -> rule2)) -> rule6)) -> rule3))]
("Erin" "is" "green" "-")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is young.
True
3
proof
[(((((triple3) -> rule2)) -> rule6) OR ((((triple3) -> rule2) ((triple3) -> rule4)) -> rule7))]
("Erin" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not young.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6) OR ((((triple3) -> rule2) ((triple3) -> rule4)) -> rule7))]
("Erin" "is" "young" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Anne" "is" "young" "+")
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is red.[(triple1)] Bob is not nice.[(triple2)] Erin is nice.[(triple3)] @1: Erin is green.[(((triple3) -> rule4) OR ((((((triple3) -> rule2)) -> rule6)) -> rule3))] Erin is round.[(((triple3) -> rule2))] @2: Erin is young.[(((((triple3) -> rule2)) -> rule6) OR ((((triple3) -> rule2) ((triple3) -> rule4)) -> rule7))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3