Bob is blue. Bob is green. Bob is quiet. Bob is red. Charlie is not green. Charlie is quiet. Charlie is rough. Charlie is young. Erin is green. Erin is quiet. Fiona is blue. Fiona is red. All young, green people are nice. Blue people are nice. All quiet people are nice. Nice people are rough. If someone is young and rough then they are quiet. All young people are red. If Erin is rough and Erin is quiet then Erin is blue. If Fiona is young and Fiona is rough then Fiona is nice. If someone is blue then they are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All young, green people are nice.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and rough then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Erin is rough and Erin is quiet then Erin is blue.
((("Erin" "is" "rough" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "blue" "+"))
If Fiona is young and Fiona is rough then Fiona is nice.
((("Fiona" "is" "young" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "nice" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule3)) -> rule4))]
("Charlie" "is" "rough" "-")
triple7
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Fiona is nice.
True
2
proof
[(((triple11) -> rule2))]
("Fiona" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple8) -> rule6))]
("Charlie" "is" "red" "-")
((triple8) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Erin is rough.
True
3
proof
[(((((triple10) -> rule3)) -> rule4))]
("Erin" "is" "rough" "+")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4) OR ((((triple3) -> rule3)) -> rule4) OR ((((((triple1) -> rule9) triple2) -> rule1)) -> rule4))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1) -> (rule9 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Erin is blue.
True
5
proof
[(((((((triple10) -> rule3)) -> rule4) triple10) -> rule7))]
("Erin" "is" "blue" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((((((triple10) -> rule3)) -> rule4) triple10) -> rule7))]
("Erin" "is" "blue" "-")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
True
6
proof
[(((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9))]
("Erin" "is" "young" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3)) triple10) -> (rule7 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is not young.
False
6
inv-proof
[(((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9))]
("Erin" "is" "young" "-")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3)) triple10) -> (rule7 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is red.
True
7
proof
[(((((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9)) -> rule6))]
("Erin" "is" "red" "+")
((((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4)) triple10) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Erin is not red.
False
7
inv-proof
[(((((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9)) -> rule6))]
("Erin" "is" "red" "-")
((((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4)) triple10) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is quiet.[(triple3 OR ((((triple1) -> rule9) ((((triple1) -> rule2)) -> rule4)) -> rule5) OR ((((triple1) -> rule9) ((((((triple1) -> rule9) triple2) -> rule1)) -> rule4)) -> rule5))] Bob is red.[(triple4 OR ((((triple1) -> rule9)) -> rule6))] Charlie is not green.[(triple5)] Charlie is quiet.[(triple6 OR ((triple8 triple7) -> rule5))] Charlie is rough.[(triple7 OR ((((triple6) -> rule3)) -> rule4))] Charlie is young.[(triple8)] Erin is green.[(triple9)] Erin is quiet.[(triple10)] Fiona is blue.[(triple11)] Fiona is red.[(triple12 OR ((((triple11) -> rule9)) -> rule6))] @1: Bob is nice.[(((triple1) -> rule2) OR ((triple3) -> rule3) OR ((((triple1) -> rule9) triple2) -> rule1))] Bob is young.[(((triple1) -> rule9))] Charlie is nice.[(((triple6) -> rule3) OR ((((triple8 triple7) -> rule5)) -> rule3))] Charlie is red.[(((triple8) -> rule6))] Erin is nice.[(((triple10) -> rule3))] Fiona is nice.[(((triple11) -> rule2))] Fiona is young.[(((triple11) -> rule9))] @2: Bob is rough.[(((((triple1) -> rule2)) -> rule4) OR ((((triple3) -> rule3)) -> rule4) OR ((((((triple1) -> rule9) triple2) -> rule1)) -> rule4))] Erin is rough.[(((((triple10) -> rule3)) -> rule4))] Fiona is rough.[(((((triple11) -> rule2)) -> rule4))] @3: Erin is blue.[(((((((triple10) -> rule3)) -> rule4) triple10) -> rule7))] Fiona is quiet.[(((((triple11) -> rule9) ((((triple11) -> rule2)) -> rule4)) -> rule5))] @4: Erin is young.[(((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9))] @5: Erin is red.[(((((((((((triple10) -> rule3)) -> rule4) triple10) -> rule7)) -> rule9)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((triple1) -> (rule9 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((triple1) -> (rule9 % int4)) ((((((triple1) -> (rule9 % int4)) triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple4
((((triple1) -> (rule9 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is not green.
("Charlie" "is" "green" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple8 triple7) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Fiona is blue.
("Fiona" "is" "blue" "+")
triple11
Fiona is red.
("Fiona" "is" "red" "+")
triple12
((((triple11) -> (rule9 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule9 % int2)) triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule9 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple8 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple8) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple11) -> (rule9 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1) -> (rule9 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple11) -> (rule9 % int4)) ((((triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3)) triple10) -> (rule7 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4)) triple10) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5