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