Anne is rough. Charlie is quiet. Erin is rough. Gary is big. Smart people are blue. If Erin is blue and Erin is red then Erin is quiet. All rough people are smart. If someone is quiet then they are furry. If someone is smart then they are furry. If someone is big then they are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Erin is blue and Erin is red then Erin is quiet.
((("Erin" "is" "blue" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "quiet" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Erin is smart.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule6))]
("Gary" "is" "rough" "-")
((triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is furry.
True
4
proof
[(((((((triple4) -> rule6)) -> rule3)) -> rule5))]
("Gary" "is" "furry" "+")
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "blue" "-")
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is rough.[(triple1)] Charlie is quiet.[(triple2)] Erin is rough.[(triple3)] Gary is big.[(triple4)] @1: Anne is smart.[(((triple1) -> rule3))] Charlie is furry.[(((triple2) -> rule4))] Erin is smart.[(((triple3) -> rule3))] Gary is rough.[(((triple4) -> rule6))] @2: Anne is blue.[(((((triple1) -> rule3)) -> rule1))] Anne is furry.[(((((triple1) -> rule3)) -> rule5))] Erin is blue.[(((((triple3) -> rule3)) -> rule1))] Erin is furry.[(((((triple3) -> rule3)) -> rule5))] Gary is smart.[(((((triple4) -> rule6)) -> rule3))] @3: Gary is blue.[(((((((triple4) -> rule6)) -> rule3)) -> rule1))] Gary is furry.[(((((((triple4) -> rule6)) -> rule3)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3