Bob is rough. Bob is white. Charlie is rough. Gary is cold. Gary is white. Harry is not green. Harry is kind. Green, cold things are kind. White things are green. If something is green then it is cold.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Green, cold things are kind.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Harry is green.
False
1
inv-proof
[(triple6)]
("Harry" "is" "green" "+")
triple6
Bob is green.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple5) -> rule2))]
("Gary" "is" "green" "-")
((triple5) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
True
4
proof
[(((((triple5) -> rule2) triple4) -> rule1) OR ((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "kind" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Bob is not cold.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is rough.[(triple1)] Bob is white.[(triple2)] Charlie is rough.[(triple3)] Gary is cold.[(triple4 OR ((((triple5) -> rule2)) -> rule3))] Gary is white.[(triple5)] Harry is kind.[(triple7)] Harry is not green.[(triple6)] @1: Bob is green.[(((triple2) -> rule2))] Gary is green.[(((triple5) -> rule2))] @2: Bob is cold.[(((((triple2) -> rule2)) -> rule3))] Gary is kind.[(((((triple5) -> rule2) triple4) -> rule1) OR ((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule3)) -> rule1))] @3: Bob is kind.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is not green.
("Harry" "is" "green" "-")
triple6
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple5) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3