Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is smart. Charlie is blue. Charlie is cold. Dave is blue. Dave is kind. Dave is nice. Erin is blue. Erin is cold. Erin is green. Erin is kind. Erin is nice. Erin is smart. All blue things are green. All nice things are blue. If something is nice then it is smart. If Charlie is nice and Charlie is blue then Charlie is red. All nice things are green. If something is red and cold then it is nice.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Charlie is nice and Charlie is blue then Charlie is red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "red" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is red and cold then it is nice.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple8 OR ((triple10) -> rule2))]
("Dave" "is" "blue" "+")
triple8
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule2))]
("Dave" "is" "blue" "-")
triple8
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1 OR ((triple3) -> rule5) OR ((((triple3) -> rule2)) -> rule1))] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is red.[(triple4)] Bob is smart.[(triple5 OR ((triple3) -> rule3))] Charlie is blue.[(triple6)] Charlie is cold.[(triple7)] Dave is blue.[(triple8 OR ((triple10) -> rule2))] Dave is kind.[(triple9)] Dave is nice.[(triple10)] Erin is blue.[(triple11 OR ((triple15) -> rule2))] Erin is cold.[(triple12)] Erin is green.[(triple13 OR ((triple11) -> rule1) OR ((triple15) -> rule5) OR ((((triple15) -> rule2)) -> rule1))] Erin is kind.[(triple14)] Erin is nice.[(triple15)] Erin is smart.[(triple16 OR ((triple15) -> rule3))] @1: Bob is blue.[(((triple3) -> rule2))] Charlie is green.[(((triple6) -> rule1))] Dave is green.[(((triple10) -> rule5) OR ((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] Dave is smart.[(((triple10) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
((triple15) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
((triple11) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple15) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple14
Erin is nice.
("Erin" "is" "nice" "+")
triple15
Erin is smart.
("Erin" "is" "smart" "+")
triple16
((triple15) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple10) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1