Bob is blue. Bob is furry. Bob is smart. Bob is white. Dave is big. Dave is blue. Dave is rough. Dave is smart. Erin is big. Erin is blue. Erin is rough. Erin is young. If something is rough then it is big. Furry things are smart. If Bob is smart and Bob is young then Bob is blue. If something is white and rough then it is smart. All smart, furry things are blue. Blue things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Bob is smart and Bob is young then Bob is blue.
((("Bob" "is" "smart" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "blue" "+"))
If something is white and rough then it is smart.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All smart, furry things are blue.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is smart.
True
1
proof
[(triple8)]
("Dave" "is" "smart" "+")
triple8
Bob is not blue.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule5) OR ((((triple2) -> rule2) triple2) -> rule5))]
("Bob" "is" "blue" "-")
triple1
((triple3 triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is blue.[(triple1 OR ((triple3 triple2) -> rule5) OR ((((triple2) -> rule2) triple2) -> rule5))] Bob is furry.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule2))] Bob is white.[(triple4)] Dave is big.[(triple5 OR ((triple7) -> rule1))] Dave is blue.[(triple6)] Dave is rough.[(triple7)] Dave is smart.[(triple8)] Erin is big.[(triple9 OR ((triple11) -> rule1))] Erin is blue.[(triple10)] Erin is rough.[(triple11)] Erin is young.[(triple12 OR ((triple10) -> rule6))] @1: Bob is young.[(((triple1) -> rule6) OR ((((triple3 triple2) -> rule5)) -> rule6) OR ((((((triple2) -> rule2) triple2) -> rule5)) -> rule6))] Dave is young.[(((triple6) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple3 triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple7) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple9
((triple11) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple2) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1