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