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