Dave is nice. Erin is blue. Erin is young. Fiona is big. Fiona is blue. Fiona is furry. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is young. Gary is blue. Gary is furry. If something is nice and big then it is blue. If something is quiet then it is big. If something is young then it is big. All red, blue things are young. Nice things are young. If something is nice and not furry then it is not quiet.
Dave is nice.
("Dave" "is" "nice" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is nice and big then it is blue.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All red, blue things are young.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is nice and not furry then it is not quiet.
((("something" "is" "nice" "+") ("something" "is" "furry" "~")) -> ("something" "is" "quiet" "-"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "young" "+")
((triple1) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "-")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "blue" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "blue" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Dave is nice.[(triple1)] Erin is blue.[(triple2)] Erin is young.[(triple3)] Fiona is big.[(triple4 OR ((triple10) -> rule3) OR ((triple8) -> rule2) OR ((((triple7) -> rule5)) -> rule3) OR ((((triple9 triple5) -> rule4)) -> rule3))] Fiona is blue.[(triple5 OR ((triple7 triple4) -> rule1) OR ((triple7 ((triple10) -> rule3)) -> rule1) OR ((triple7 ((triple8) -> rule2)) -> rule1) OR ((triple7 ((((triple7) -> rule5)) -> rule3)) -> rule1))] Fiona is furry.[(triple6)] Fiona is nice.[(triple7)] Fiona is quiet.[(triple8)] Fiona is red.[(triple9)] Fiona is young.[(triple10 OR ((triple7) -> rule5) OR ((triple9 triple5) -> rule4) OR ((triple9 ((triple7 triple4) -> rule1)) -> rule4) OR ((triple9 ((triple7 ((triple8) -> rule2)) -> rule1)) -> rule4))] Gary is blue.[(triple11)] Gary is furry.[(triple12)] @1: Dave is young.[(((triple1) -> rule5))] Erin is big.[(((triple3) -> rule3))] @2: Dave is big.[(((((triple1) -> rule5)) -> rule3))] @3: Dave is blue.[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
((triple10) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple7 triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple7 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
((triple7) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9 triple5) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9 ((triple7 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple9 ((triple7 ((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3