Dave is big. Dave is smart. Fiona is green. Fiona is not red. Gary is quiet. Harry is green. Harry is nice. All nice people are blue. Green people are nice. Quiet, big people are not nice. Nice, blue people are smart. All big people are green. Nice people are green. If someone is big and blue then they are not quiet. If someone is smart and not red then they are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Quiet, big people are not nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
Nice, blue people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is big and blue then they are not quiet.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "-"))
If someone is smart and not red then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple2 OR ((((((triple1) -> rule5)) -> rule2) ((((((triple1) -> rule5)) -> rule2)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "+")
triple2
((((((triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Harry is not nice.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule2))]
("Harry" "is" "nice" "-")
triple7
((triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is green.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "green" "+")
((triple1) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "green" "-")
((triple1) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is smart.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4))]
("Fiona" "is" "smart" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Dave is not blue.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is big.
True
8
proof
[(((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4) triple4) -> rule8))]
("Fiona" "is" "big" "+")
((((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Dave is quiet.
False
6
inv-proof
[(((triple1 ((((((triple1) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
("Dave" "is" "quiet" "+")
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is not quiet.
True
12
proof
[(((((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4) triple4) -> rule8) ((((triple3) -> rule2)) -> rule1)) -> rule7))]
("Fiona" "is" "quiet" "-")
((((((((triple3) -> (rule2 % int5)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple4) -> (rule8 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is quiet.
False
12
inv-proof
[(((((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4) triple4) -> rule8) ((((triple3) -> rule2)) -> rule1)) -> rule7))]
("Fiona" "is" "quiet" "+")
((((((((triple3) -> (rule2 % int5)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple4) -> (rule8 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Gary is not nice.
Unknown
inv-rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule8 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not green.
Unknown
inv-rconc
[@4: Gary is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- rule8 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is smart.
Unknown
rconc
[@4: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- rule8 <- FAIL)]]
("Gary" "is" "smart" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "big" "-")
Gary is blue.
Unknown
rconc
[@4: Gary is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- rule8 <- FAIL)]]
("Gary" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Dave is big.[(triple1)] Dave is smart.[(triple2 OR ((((((triple1) -> rule5)) -> rule2) ((((((triple1) -> rule5)) -> rule2)) -> rule1)) -> rule4))] Fiona is green.[(triple3)] Fiona is not red.[(triple4)] Gary is quiet.[(triple5)] Harry is green.[(triple6 OR ((triple7) -> rule6))] Harry is nice.[(triple7 OR ((triple6) -> rule2))] @1: Dave is green.[(((triple1) -> rule5))] Fiona is nice.[(((triple3) -> rule2))] Harry is blue.[(((triple7) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] @2: Dave is nice.[(((((triple1) -> rule5)) -> rule2))] Fiona is blue.[(((((triple3) -> rule2)) -> rule1))] Harry is smart.[(((triple7 ((triple7) -> rule1)) -> rule4) OR ((((triple6) -> rule2) ((triple7) -> rule1)) -> rule4) OR ((triple7 ((((triple6) -> rule2)) -> rule1)) -> rule4) OR ((((triple6) -> rule2) ((((triple6) -> rule2)) -> rule1)) -> rule4))] @3: Dave is blue.[(((((((triple1) -> rule5)) -> rule2)) -> rule1))] Fiona is smart.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4))] @4: Dave is not quiet.[(((triple1 ((((((triple1) -> rule5)) -> rule2)) -> rule1)) -> rule7))] Fiona is big.[(((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4) triple4) -> rule8))] @5: Fiona is not quiet.[(((((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule4) triple4) -> rule8) ((((triple3) -> rule2)) -> rule1)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
((((((triple1) -> (rule5 % int4))) -> (rule2 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is not red.
("Fiona" "is" "red" "-")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple7 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple6) -> (rule2 % int3)) ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((((((triple3) -> (rule2 % int5)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple4) -> (rule8 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5