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