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