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