Bob is big. Charlie is green. Erin is quiet. Quiet things are cold. All big, kind things are quiet. If something is kind and red then it is big. If something is quiet and big then it is kind. Quiet things are green. All kind, quiet things are blue. All green, cold things are kind. If something is red then it is blue.
Bob is big.
("Bob" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All big, kind things are quiet.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and red then it is big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is quiet and big then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All kind, quiet things are blue.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All green, cold things are kind.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Erin is cold.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "green" "-")
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
True
5
proof
[(((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7))]
("Erin" "is" "kind" "+")
((((triple3) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7))]
("Erin" "is" "kind" "-")
((((triple3) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is blue.
True
7
proof
[(((((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7) triple3) -> rule6))]
("Erin" "is" "blue" "+")
((((((triple3) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule7 % int2)) triple3) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is not blue.
False
7
inv-proof
[(((((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7) triple3) -> rule6))]
("Erin" "is" "blue" "-")
((((((triple3) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule7 % int2)) triple3) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@3: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule5 <- FAIL)]]
("Bob" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is kind.
Unknown
rconc
[@4: Charlie is kind.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is big.[(triple1)] Charlie is green.[(triple2)] Erin is quiet.[(triple3)] @1: Erin is cold.[(((triple3) -> rule1))] Erin is green.[(((triple3) -> rule5))] @2: Erin is kind.[(((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7))] @3: Erin is blue.[(((((((triple3) -> rule5) ((triple3) -> rule1)) -> rule7) triple3) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple3) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple3) -> (rule5 % int4)) ((triple3) -> (rule1 % int3))) -> (rule7 % int2)) triple3) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4