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