Dave is blue. Dave is furry. Dave is smart. Dave is young. Erin is blue. Erin is furry. Erin is green. Erin is nice. Erin is red. Erin is smart. Erin is young. Fiona is green. Fiona is young. Gary is green. Gary is red. Gary is smart. Red people are young. Nice, furry people are green. If someone is nice then they are young. All furry people are nice. All green people are red. All smart, furry people are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Nice, furry people are green.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All smart, furry people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Gary is red.
True
1
proof
[(triple15 OR ((triple14) -> rule5))]
("Gary" "is" "red" "+")
triple15
((triple14) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
Gary is young.
True
2
proof
[(((triple15) -> rule1) OR ((((triple14) -> rule5)) -> rule1))]
("Gary" "is" "young" "+")
((triple15) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("Dave" "is" "green" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule2))]
("Dave" "is" "green" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
("Dave" "is" "red" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not red.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
("Dave" "is" "red" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Dave is blue.[(triple1 OR ((triple3 triple2) -> rule6))] Dave is furry.[(triple2)] Dave is smart.[(triple3)] Dave is young.[(triple4 OR ((((triple2) -> rule4)) -> rule3) OR ((((((((triple2) -> rule4) triple2) -> rule2)) -> rule5)) -> rule1))] Erin is blue.[(triple5 OR ((triple10 triple6) -> rule6))] Erin is furry.[(triple6)] Erin is green.[(triple7 OR ((triple8 triple6) -> rule2) OR ((((triple6) -> rule4) triple6) -> rule2))] Erin is nice.[(triple8 OR ((triple6) -> rule4))] Erin is red.[(triple9 OR ((triple7) -> rule5) OR ((((triple8 triple6) -> rule2)) -> rule5) OR ((((((triple6) -> rule4) triple6) -> rule2)) -> rule5))] Erin is smart.[(triple10)] Erin is young.[(triple11 OR ((triple8) -> rule3) OR ((triple9) -> rule1) OR ((((triple6) -> rule4)) -> rule3) OR ((((triple7) -> rule5)) -> rule1) OR ((((((triple8 triple6) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple6) -> rule4) triple6) -> rule2)) -> rule5)) -> rule1))] Fiona is green.[(triple12)] Fiona is young.[(triple13 OR ((((triple12) -> rule5)) -> rule1))] Gary is green.[(triple14)] Gary is red.[(triple15 OR ((triple14) -> rule5))] Gary is smart.[(triple16)] @1: Dave is nice.[(((triple2) -> rule4))] Fiona is red.[(((triple12) -> rule5))] Gary is young.[(((triple15) -> rule1) OR ((((triple14) -> rule5)) -> rule1))] @2: Dave is green.[(((((triple2) -> rule4) triple2) -> rule2))] @3: Dave is red.[(((((((triple2) -> rule4) triple2) -> rule2)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((((triple2) -> (rule4 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
((triple10 triple6) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple8 triple6) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple6) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple9
((triple7) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple8 triple6) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple6) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple11
((triple8) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple8 triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((((triple6) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple12
Fiona is young.
("Fiona" "is" "young" "+")
triple13
((((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is red.
("Gary" "is" "red" "+")
triple15
((triple14) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple16
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple12) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple15) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3