Dave is round. Fiona is blue. Fiona is furry. Fiona is smart. Gary is blue. Gary is furry. Gary is kind. Gary is nice. Gary is round. Gary is young. All blue people are furry. All round people are furry. All young, furry people are kind. Furry people are young. If someone is kind and not nice then they are smart. All nice people are blue.
Dave is round.
("Dave" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All young, furry people are kind.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not nice then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "smart" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Gary is round.
True
1
proof
[(triple9)]
("Gary" "is" "round" "+")
triple9
Gary is not round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "-")
triple9
Dave is furry.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((triple2) -> rule1)) -> rule4))]
("Fiona" "is" "young" "-")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule3) OR ((((triple3) -> rule4) ((triple2) -> rule1)) -> rule3) OR ((((((triple2) -> rule1)) -> rule4) triple3) -> rule3) OR ((((((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "kind" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Dave is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Dave" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
True
6
proof
[(((((((triple1) -> rule2)) -> rule4) ((triple1) -> rule2)) -> rule3))]
("Dave" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not kind.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule4) ((triple1) -> rule2)) -> rule3))]
("Dave" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "blue" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Dave is round.[(triple1)] Fiona is blue.[(triple2)] Fiona is furry.[(triple3 OR ((triple2) -> rule1))] Fiona is smart.[(triple4)] Gary is blue.[(triple5 OR ((triple8) -> rule6))] Gary is furry.[(triple6 OR ((triple5) -> rule1) OR ((triple9) -> rule2) OR ((((triple8) -> rule6)) -> rule1))] Gary is kind.[(triple7 OR ((triple10 triple6) -> rule3) OR ((triple10 ((triple5) -> rule1)) -> rule3) OR ((triple10 ((triple9) -> rule2)) -> rule3) OR ((((triple6) -> rule4) triple6) -> rule3) OR ((((triple6) -> rule4) ((triple5) -> rule1)) -> rule3) OR ((((triple6) -> rule4) ((triple9) -> rule2)) -> rule3) OR ((triple10 ((((triple8) -> rule6)) -> rule1)) -> rule3) OR ((((((triple5) -> rule1)) -> rule4) triple6) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) triple6) -> rule3) OR ((((triple6) -> rule4) ((((triple8) -> rule6)) -> rule1)) -> rule3) OR ((((((triple5) -> rule1)) -> rule4) ((triple5) -> rule1)) -> rule3) OR ((((((triple5) -> rule1)) -> rule4) ((triple9) -> rule2)) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) ((triple5) -> rule1)) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) ((triple9) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule4) ((((triple8) -> rule6)) -> rule1)) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) ((((triple8) -> rule6)) -> rule1)) -> rule3) OR ((((((((triple8) -> rule6)) -> rule1)) -> rule4) triple6) -> rule3) OR ((((((((triple8) -> rule6)) -> rule1)) -> rule4) ((triple5) -> rule1)) -> rule3) OR ((((((((triple8) -> rule6)) -> rule1)) -> rule4) ((triple9) -> rule2)) -> rule3) OR ((((((((triple8) -> rule6)) -> rule1)) -> rule4) ((((triple8) -> rule6)) -> rule1)) -> rule3))] Gary is nice.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10 OR ((triple6) -> rule4) OR ((((triple5) -> rule1)) -> rule4) OR ((((triple9) -> rule2)) -> rule4) OR ((((((triple8) -> rule6)) -> rule1)) -> rule4))] @1: Dave is furry.[(((triple1) -> rule2))] Fiona is young.[(((triple3) -> rule4) OR ((((triple2) -> rule1)) -> rule4))] @2: Dave is young.[(((((triple1) -> rule2)) -> rule4))] Fiona is kind.[(((((triple3) -> rule4) triple3) -> rule3) OR ((((triple3) -> rule4) ((triple2) -> rule1)) -> rule3) OR ((((((triple2) -> rule1)) -> rule4) triple3) -> rule3) OR ((((((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule3))] @3: Dave is kind.[(((((((triple1) -> rule2)) -> rule4) ((triple1) -> rule2)) -> rule3))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
((triple8) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple5) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple10 triple6) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple10 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple10 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple6) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
((((triple6) -> (rule4 % int3)) ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
((triple10 ((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple6) -> (rule4 % int4)) ((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((((triple5) -> (rule1 % int3))) -> (rule4 % int2)) ((triple5) -> (rule1 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule4 % int2)) ((triple9) -> (rule2 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) ((triple5) -> (rule1 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) ((triple9) -> (rule2 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple5) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple8) -> (rule6 % int2))) -> (rule1 % int4))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((((triple9) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple8) -> (rule6 % int2))) -> (rule1 % int4))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple5) -> (rule1 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple9) -> (rule2 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple6) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3