Bob is green. Charlie is big. Dave is cold. Fiona is cold. Green, smart things are big. If something is smart and green then it is cold. Rough things are big. If something is big then it is blue. All blue things are cold. Blue, cold things are white.
Bob is green.
("Bob" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Green, smart things are big.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is smart and green then it is cold.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Blue, cold things are white.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Charlie is blue.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Charlie" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Charlie" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is white.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Charlie" "is" "white" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not white.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is cold.
Unknown
rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is green.[(triple1)] Charlie is big.[(triple2)] Dave is cold.[(triple3)] Fiona is cold.[(triple4)] @1: Charlie is blue.[(((triple2) -> rule4))] @2: Charlie is cold.[(((((triple2) -> rule4)) -> rule5))] @3: Charlie is white.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule5)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3