Charlie is big. Erin is big. Erin is cold. Erin is white. Erin is young. Fiona is cold. Gary is young. If someone is nice then they are white. White people are big. If someone is cold then they are nice. White people are round. All young, cold people are white. If someone is nice and white then they are cold. If Charlie is round and Charlie is big then Charlie is nice. Round people are white.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is nice then they are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All young, cold people are white.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and white then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is round and Charlie is big then Charlie is nice.
((("Charlie" "is" "round" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "nice" "+"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Erin is not cold.
False
1
inv-proof
[(triple3)]
("Erin" "is" "cold" "-")
triple3
Erin is nice.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple5 triple3) -> rule5)) -> rule4) OR ((((((triple3) -> rule3)) -> rule1)) -> rule4))]
("Erin" "is" "round" "-")
((triple4) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Fiona is white.
True
3
proof
[(((((triple6) -> rule3)) -> rule1))]
("Fiona" "is" "white" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not white.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule1))]
("Fiona" "is" "white" "-")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is big.
True
4
proof
[(((((((triple6) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not round.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule1)) -> rule4))]
("Fiona" "is" "round" "-")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@6: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule7 <- rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Gary is round.
Unknown
rconc
[@4: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- rule6 <- FAIL)]]
("Gary" "is" "round" "+")
Charlie is not round.
Unknown
inv-rconc
[@5: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- rule6 <- rule7 <- FAIL)]]
("Charlie" "is" "round" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Charlie is big.[(triple1)] Erin is big.[(triple2 OR ((triple4) -> rule2) OR ((((triple5 triple3) -> rule5)) -> rule2) OR ((((((triple3) -> rule3)) -> rule1)) -> rule2))] Erin is cold.[(triple3)] Erin is white.[(triple4 OR ((triple5 triple3) -> rule5) OR ((((triple3) -> rule3)) -> rule1))] Erin is young.[(triple5)] Fiona is cold.[(triple6)] Gary is young.[(triple7)] @1: Erin is nice.[(((triple3) -> rule3))] Erin is round.[(((triple4) -> rule4) OR ((((triple5 triple3) -> rule5)) -> rule4) OR ((((((triple3) -> rule3)) -> rule1)) -> rule4))] Fiona is nice.[(((triple6) -> rule3))] @2: Fiona is white.[(((((triple6) -> rule3)) -> rule1))] @3: Fiona is big.[(((((((triple6) -> rule3)) -> rule1)) -> rule2))] Fiona is round.[(((((((triple6) -> rule3)) -> rule1)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
((triple4) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple5 triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
((triple5 triple3) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple4) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3