Dave is big. Dave is nice. Dave is red. Fiona is quiet. Gary is quiet. Gary is red. Harry is big. Harry is furry. Harry is red. Harry is round. All green things are red. Red things are green. All furry, quiet things are green. Furry, big things are round. If something is green then it is big. All red, nice things are round. If Harry is green then Harry is quiet. If something is furry then it is quiet.
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All furry, quiet things are green.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Furry, big things are round.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All red, nice things are round.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Harry is green then Harry is quiet.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "quiet" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple7 OR ((((triple9) -> rule2)) -> rule5) OR ((((triple8 ((triple8) -> rule8)) -> rule3)) -> rule5))]
("Harry" "is" "big" "+")
triple7
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Fiona is not quiet.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "quiet" "-")
triple4
Fiona is not green.
Unknown
inv-rconc
[@3: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Dave is big.[(triple1 OR ((((triple3) -> rule2)) -> rule5))] Dave is nice.[(triple2)] Dave is red.[(triple3)] Fiona is quiet.[(triple4)] Gary is quiet.[(triple5)] Gary is red.[(triple6)] Harry is big.[(triple7 OR ((((triple9) -> rule2)) -> rule5) OR ((((triple8 ((triple8) -> rule8)) -> rule3)) -> rule5))] Harry is furry.[(triple8)] Harry is red.[(triple9 OR ((((triple8 ((triple8) -> rule8)) -> rule3)) -> rule1))] Harry is round.[(triple10 OR ((triple8 triple7) -> rule4) OR ((triple8 ((((triple9) -> rule2)) -> rule5)) -> rule4) OR ((triple8 ((((triple8 ((triple8) -> rule8)) -> rule3)) -> rule5)) -> rule4))] @1: Dave is green.[(((triple3) -> rule2))] Dave is round.[(((triple3 triple2) -> rule6))] Gary is green.[(((triple6) -> rule2))] Harry is green.[(((triple9) -> rule2) OR ((triple8 ((triple8) -> rule8)) -> rule3))] Harry is quiet.[(((triple8) -> rule8) OR ((((triple9) -> rule2)) -> rule7))] @2: Gary is big.[(((((triple6) -> rule2)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple8 triple7) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple8 ((((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple8 ((((triple8 ((triple8) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple8 ((triple8) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple8) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2