Anne is big. Anne is nice. Anne is rough. Anne is not round. Charlie is round. Charlie is smart. Erin is cold. Erin is rough. Erin is not smart. Gary is big. If Erin is big and Erin is furry then Erin is rough. If someone is smart and nice then they are rough. If someone is cold then they are nice. If someone is smart then they are cold. All smart, big people are not cold. If someone is rough and not big then they are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not round.
("Anne" "is" "round" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is big.
("Gary" "is" "big" "+")
If Erin is big and Erin is furry then Erin is rough.
((("Erin" "is" "big" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "rough" "+"))
If someone is smart and nice then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All smart, big people are not cold.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
If someone is rough and not big then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
Gary is big.
True
1
proof
[(triple10)]
("Gary" "is" "big" "+")
triple10
Charlie is not round.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "round" "-")
triple5
Charlie is cold.
True
2
proof
[(((triple6) -> rule4))]
("Charlie" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple6) -> rule4))]
("Charlie" "is" "cold" "-")
((triple6) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple6) -> rule4)) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule3))]
("Charlie" "is" "nice" "-")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
True
5
proof
[(((triple6 ((((triple6) -> rule4)) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple6 ((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not rough.
False
5
inv-proof
[(((triple6 ((((triple6) -> rule4)) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "-")
((triple6 ((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "cold" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is not round.[(triple4)] Anne is rough.[(triple3)] Charlie is round.[(triple5)] Charlie is smart.[(triple6)] Erin is cold.[(triple7)] Erin is not smart.[(triple9)] Erin is rough.[(triple8)] Gary is big.[(triple10)] @1: Charlie is cold.[(((triple6) -> rule4))] Erin is nice.[(((triple7) -> rule3))] @2: Charlie is nice.[(((((triple6) -> rule4)) -> rule3))] @3: Charlie is rough.[(((triple6 ((((triple6) -> rule4)) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not round.
("Anne" "is" "round" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is not smart.
("Erin" "is" "smart" "-")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple10
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple7) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple6 ((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3