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