Bob is green. Bob is quiet. Bob is smart. Bob is young. Gary is blue. Gary is cold. Gary is young. If Gary is young and Gary is blue then Gary is cold. Smart things are not round. Smart, round things are not young. All cold things are smart. If Gary is not green then Gary is not blue. If something is green and not young then it is quiet.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is young and Gary is blue then Gary is cold.
((("Gary" "is" "young" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "cold" "+"))
Smart things are not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
Smart, round things are not young.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "-"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Gary is not green then Gary is not blue.
((("Gary" "is" "green" "~")) -> ("Gary" "is" "blue" "-"))
If something is green and not young then it is quiet.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "quiet" "+"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Gary is not cold.
False
1
inv-proof
[(triple6 OR ((triple7 triple5) -> rule1))]
("Gary" "is" "cold" "-")
triple6
((triple7 triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Bob is not round.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is round.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "+")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Gary is not round.
True
3
proof
[(((((triple6) -> rule4)) -> rule2) OR ((((((triple7 triple5) -> rule1)) -> rule4)) -> rule2))]
("Gary" "is" "round" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple7 triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule2) OR ((((((triple7 triple5) -> rule1)) -> rule4)) -> rule2))]
("Gary" "is" "round" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple7 triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "quiet" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3)] Bob is young.[(triple4)] Gary is blue.[(triple5)] Gary is cold.[(triple6 OR ((triple7 triple5) -> rule1))] Gary is young.[(triple7)] @1: Bob is not round.[(((triple3) -> rule2))] Gary is smart.[(((triple6) -> rule4) OR ((((triple7 triple5) -> rule1)) -> rule4))] @2: Gary is not round.[(((((triple6) -> rule4)) -> rule2) OR ((((((triple7 triple5) -> rule1)) -> rule4)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple7 triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is not round.
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple7 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple7 triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3