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