Charlie is big. Charlie is kind. Charlie is quiet. Dave is blue. Dave is kind. Dave is red. Dave is rough. Fiona is big. Fiona is kind. Fiona is quiet. Harry is big. Harry is red. If someone is blue then they are kind. All big, nice people are quiet. If someone is kind and quiet then they are nice. Kind people are quiet. If someone is rough then they are quiet. All big people are kind. Nice people are red. If someone is kind then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All big, nice people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and quiet then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple5 OR ((triple4) -> rule1))]
("Dave" "is" "kind" "+")
triple5
((triple4) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not rough.
False
1
inv-proof
[(triple7)]
("Dave" "is" "rough" "-")
triple7
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule8))] Charlie is kind.[(triple2 OR ((triple1) -> rule6))] Charlie is quiet.[(triple3 OR ((triple2) -> rule4) OR ((((triple1) -> rule6)) -> rule4))] Dave is blue.[(triple4)] Dave is kind.[(triple5 OR ((triple4) -> rule1))] Dave is red.[(triple6 OR ((((triple5 ((triple5) -> rule4)) -> rule3)) -> rule7) OR ((((triple5 ((triple7) -> rule5)) -> rule3)) -> rule7) OR ((((((triple4) -> rule1) ((triple5) -> rule4)) -> rule3)) -> rule7) OR ((((((triple4) -> rule1) ((triple7) -> rule5)) -> rule3)) -> rule7) OR ((((triple5 ((((triple4) -> rule1)) -> rule4)) -> rule3)) -> rule7) OR ((((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule4)) -> rule3)) -> rule7))] Dave is rough.[(triple7)] Fiona is big.[(triple8 OR ((triple9) -> rule8))] Fiona is kind.[(triple9 OR ((triple8) -> rule6))] Fiona is quiet.[(triple10 OR ((triple9) -> rule4) OR ((((triple8) -> rule6)) -> rule4))] Harry is big.[(triple11)] Harry is red.[(triple12 OR ((((((triple11) -> rule6) ((((triple11) -> rule6)) -> rule4)) -> rule3)) -> rule7))] @1: Charlie is nice.[(((triple2 triple3) -> rule3) OR ((triple2 ((triple2) -> rule4)) -> rule3) OR ((((triple1) -> rule6) triple3) -> rule3) OR ((((triple1) -> rule6) ((triple2) -> rule4)) -> rule3) OR ((triple2 ((((triple1) -> rule6)) -> rule4)) -> rule3) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule4)) -> rule3))] Dave is big.[(((triple5) -> rule8) OR ((((triple4) -> rule1)) -> rule8))] Dave is quiet.[(((triple5) -> rule4) OR ((triple7) -> rule5) OR ((((triple4) -> rule1)) -> rule4))] Fiona is nice.[(((triple9 triple10) -> rule3) OR ((triple9 ((triple9) -> rule4)) -> rule3) OR ((((triple8) -> rule6) triple10) -> rule3) OR ((((triple8) -> rule6) ((triple9) -> rule4)) -> rule3) OR ((triple9 ((((triple8) -> rule6)) -> rule4)) -> rule3) OR ((((triple8) -> rule6) ((((triple8) -> rule6)) -> rule4)) -> rule3))] Harry is kind.[(((triple11) -> rule6))] @2: Charlie is red.[(((((triple2 triple3) -> rule3)) -> rule7) OR ((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule7) OR ((((((triple1) -> rule6) triple3) -> rule3)) -> rule7) OR ((((((triple1) -> rule6) ((triple2) -> rule4)) -> rule3)) -> rule7) OR ((((triple2 ((((triple1) -> rule6)) -> rule4)) -> rule3)) -> rule7) OR ((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule4)) -> rule3)) -> rule7))] Dave is nice.[(((triple5 ((triple5) -> rule4)) -> rule3) OR ((triple5 ((triple7) -> rule5)) -> rule3) OR ((((triple4) -> rule1) ((triple5) -> rule4)) -> rule3) OR ((((triple4) -> rule1) ((triple7) -> rule5)) -> rule3) OR ((triple5 ((((triple4) -> rule1)) -> rule4)) -> rule3) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule4)) -> rule3))] Fiona is red.[(((((triple9 triple10) -> rule3)) -> rule7) OR ((((triple9 ((triple9) -> rule4)) -> rule3)) -> rule7) OR ((((((triple8) -> rule6) triple10) -> rule3)) -> rule7) OR ((((((triple8) -> rule6) ((triple9) -> rule4)) -> rule3)) -> rule7) OR ((((triple9 ((((triple8) -> rule6)) -> rule4)) -> rule3)) -> rule7) OR ((((((triple8) -> rule6) ((((triple8) -> rule6)) -> rule4)) -> rule3)) -> rule7))] Harry is quiet.[(((((triple11) -> rule6)) -> rule4))] @3: Harry is nice.[(((((triple11) -> rule6) ((((triple11) -> rule6)) -> rule4)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple1) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((triple4) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple6
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple5 ((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple4) -> (rule1 % int4)) ((triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((triple4) -> (rule1 % int4)) ((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((triple5 ((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple9) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
((triple8) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
((triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((((((triple11) -> (rule6 % int4)) ((((triple11) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2 triple3) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((triple2 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple9 triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple9 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple8) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple8) -> (rule6 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((triple9 ((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((triple11) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2 triple3) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple1) -> (rule6 % int4)) ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple2 ((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple5 ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple4) -> (rule1 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((triple9 triple10) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple9 ((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((((triple8) -> (rule6 % int3)) triple10) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((triple8) -> (rule6 % int4)) ((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple9 ((((triple8) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((((triple8) -> (rule6 % int4)) ((((triple8) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple11) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple11) -> (rule6 % int3)) ((((triple11) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3