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