Anne is nice. Charlie is red. Erin is rough. All big people are red. If someone is rough and red then they are furry. Rough people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and red then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Erin is big.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "-")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Erin" "is" "furry" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not furry.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Erin" "is" "furry" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is red.
Unknown
rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "red" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Charlie is red.[(triple2)] Erin is rough.[(triple3)] @1: Erin is big.[(((triple3) -> rule3))] @2: Erin is red.[(((((triple3) -> rule3)) -> rule1))] @3: Erin is furry.[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3