Anne is green. Erin is furry. Gary is nice. All big, smart people are nice. If Gary is nice then Gary is smart. Big, smart people are green. Cold, smart people are nice. If someone is smart then they are cold. All green people are smart.
Anne is green.
("Anne" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All big, smart people are nice.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Gary is nice then Gary is smart.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
Big, smart people are green.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Cold, smart people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is smart.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
True
6
proof
[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not nice.
False
6
inv-proof
[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is nice.
Unknown
rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Erin is furry.[(triple2)] Gary is nice.[(triple3)] @1: Anne is smart.[(((triple1) -> rule6))] Gary is smart.[(((triple3) -> rule2))] @2: Anne is cold.[(((((triple1) -> rule6)) -> rule5))] Gary is cold.[(((((triple3) -> rule2)) -> rule5))] @3: Anne is nice.[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3