Charlie is nice. Erin is white. Gary is nice. All big people are white. If Erin is round then Erin is young. Young people are quiet. If Erin is cold and Erin is young then Erin is quiet. If someone is white and young then they are nice. Nice people are big. If Erin is young and Erin is cold then Erin is big. White, big people are cold.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Erin is round then Erin is young.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "young" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is cold and Erin is young then Erin is quiet.
((("Erin" "is" "cold" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is white and young then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Erin is young and Erin is cold then Erin is big.
((("Erin" "is" "young" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "big" "+"))
White, big people are cold.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Gary is big.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "big" "-")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is not big.
Unknown
inv-rconc
[@3: Erin is big.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is nice.[(triple1)] Erin is white.[(triple2)] Gary is nice.[(triple3)] @1: Charlie is big.[(((triple1) -> rule6))] Gary is big.[(((triple3) -> rule6))] @2: Charlie is white.[(((((triple1) -> rule6)) -> rule1))] Gary is white.[(((((triple3) -> rule6)) -> rule1))] @3: Charlie is cold.[(((((((triple1) -> rule6)) -> rule1) ((triple1) -> rule6)) -> rule8))] Gary is cold.[(((((((triple3) -> rule6)) -> rule1) ((triple3) -> rule6)) -> rule8))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2)) ((triple1) -> (rule6 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3) -> (rule6 % int3))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3