Charlie is quiet. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. Fiona is furry. Fiona is quiet. Fiona is rough. Fiona is smart. Fiona is young. Harry is furry. Harry is quiet. Harry is rough. Harry is round. Harry is white. Quiet, young things are smart. Rough, smart things are young. If Fiona is rough and Fiona is young then Fiona is white. All white, young things are rough. If Harry is quiet then Harry is young. If something is round and white then it is quiet.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Quiet, young things are smart.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Rough, smart things are young.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Fiona is rough and Fiona is young then Fiona is white.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "white" "+"))
All white, young things are rough.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Harry is quiet then Harry is young.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "young" "+"))
If something is round and white then it is quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Charlie is smart.
True
1
proof
[(triple3 OR ((triple1 triple5) -> rule1) OR ((((triple2 triple4) -> rule6) triple5) -> rule1))]
("Charlie" "is" "smart" "+")
triple3
((triple1 triple5) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple2 triple4) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Charlie is rough.
True
3
proof
[(((triple4 triple5) -> rule4))]
("Charlie" "is" "rough" "+")
((triple4 triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
3
inv-proof
[(((triple4 triple5) -> rule4))]
("Charlie" "is" "rough" "-")
((triple4 triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is smart.
True
4
proof
[(((triple12 ((triple12) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((triple12) -> rule5)) -> rule1) OR ((triple12 ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1))]
("Harry" "is" "smart" "+")
((triple12 ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple14 triple15) -> (rule6 % int3)) ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((triple12 ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple14 triple15) -> (rule6 % int3)) ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((triple12 ((triple12) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((triple12) -> rule5)) -> rule1) OR ((triple12 ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1))]
("Harry" "is" "smart" "-")
((triple12 ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple14 triple15) -> (rule6 % int3)) ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((triple12 ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple14 triple15) -> (rule6 % int3)) ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is quiet.[(triple1 OR ((triple2 triple4) -> rule6))] Charlie is round.[(triple2)] Charlie is smart.[(triple3 OR ((triple1 triple5) -> rule1) OR ((((triple2 triple4) -> rule6) triple5) -> rule1))] Charlie is white.[(triple4)] Charlie is young.[(triple5)] Fiona is furry.[(triple6)] Fiona is quiet.[(triple7)] Fiona is rough.[(triple8)] Fiona is smart.[(triple9 OR ((triple7 triple10) -> rule1))] Fiona is young.[(triple10 OR ((triple8 triple9) -> rule2))] Harry is furry.[(triple11)] Harry is quiet.[(triple12 OR ((triple14 triple15) -> rule6))] Harry is rough.[(triple13 OR ((triple15 ((triple12) -> rule5)) -> rule4) OR ((triple15 ((((triple14 triple15) -> rule6)) -> rule5)) -> rule4))] Harry is round.[(triple14)] Harry is white.[(triple15)] @1: Charlie is rough.[(((triple4 triple5) -> rule4))] Fiona is white.[(((triple8 triple10) -> rule3) OR ((triple8 ((triple8 triple9) -> rule2)) -> rule3))] Harry is young.[(((triple12) -> rule5) OR ((((triple14 triple15) -> rule6)) -> rule5))] @2: Harry is smart.[(((triple12 ((triple12) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((triple12) -> rule5)) -> rule1) OR ((triple12 ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1) OR ((((triple14 triple15) -> rule6) ((((triple14 triple15) -> rule6)) -> rule5)) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
((triple2 triple4) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple1 triple5) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple2 triple4) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
((triple7 triple10) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple10
((triple8 triple9) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
((triple14 triple15) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple13
((triple15 ((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple15 ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4 triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple8 triple10) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple8 ((triple8 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple14 triple15) -> (rule6 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple12 ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple14 triple15) -> (rule6 % int3)) ((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((triple12 ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple14 triple15) -> (rule6 % int3)) ((((triple14 triple15) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3