Bob is blue. Charlie is cold. Gary is green. All cold people are quiet. If someone is green then they are kind. If Gary is blue and Gary is cold then Gary is big. Big people are blue. All blue people are quiet. If Gary is kind then Gary is cold.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Gary is blue and Gary is cold then Gary is big.
((("Gary" "is" "blue" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "big" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is kind then Gary is cold.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "cold" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Gary is kind.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("Gary" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule1))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule1))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Charlie is cold.[(triple2)] Gary is green.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule5))] Charlie is quiet.[(((triple2) -> rule1))] Gary is kind.[(((triple3) -> rule2))] @2: Gary is cold.[(((((triple3) -> rule2)) -> rule6))] @3: Gary is quiet.[(((((((triple3) -> rule2)) -> rule6)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3