Bob is kind. Bob is quiet. Bob is young. Erin is kind. Erin is rough. Erin is smart. Fiona is red. Harry is not red. Harry is round. Harry is young. All young things are quiet. Red, kind things are quiet. If something is smart then it is not quiet. If something is round then it is young. Quiet, young things are rough. If something is young and kind then it is rough. Rough things are kind. If Bob is round and Bob is rough then Bob is smart. Red things are round.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Red, kind things are quiet.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is smart then it is not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Quiet, young things are rough.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is young and kind then it is rough.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Bob is round and Bob is rough then Bob is smart.
((("Bob" "is" "round" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "smart" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Fiona is red.
True
1
proof
[(triple7)]
("Fiona" "is" "red" "+")
triple7
Harry is not round.
False
1
inv-proof
[(triple9)]
("Harry" "is" "round" "-")
triple9
Fiona is round.
True
2
proof
[(((triple7) -> rule9))]
("Fiona" "is" "round" "+")
((triple7) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Bob is not rough.
False
3
inv-proof
[(((triple2 triple3) -> rule5) OR ((triple3 triple1) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule5))]
("Bob" "is" "rough" "-")
((triple2 triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 triple1) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Fiona is young.
True
3
proof
[(((((triple7) -> rule9)) -> rule4))]
("Fiona" "is" "young" "+")
((((triple7) -> (rule9 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((((triple10) -> rule1) triple10) -> rule5) OR ((((triple10) -> rule1) ((triple9) -> rule4)) -> rule5) OR ((((((triple9) -> rule4)) -> rule1) triple10) -> rule5) OR ((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule4)) -> rule5))]
("Harry" "is" "rough" "-")
((((triple10) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2)) ((triple9) -> (rule4 % int3))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Fiona is quiet.
True
4
proof
[(((((((triple7) -> rule9)) -> rule4)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((((triple7) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not quiet.
False
4
inv-proof
[(((((((triple7) -> rule9)) -> rule4)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((((triple7) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
True
8
proof
[(((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5))]
("Fiona" "is" "rough" "+")
((((((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is not rough.
False
8
inv-proof
[(((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5))]
("Fiona" "is" "rough" "-")
((((((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is kind.
True
9
proof
[(((((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5)) -> rule7))]
("Fiona" "is" "kind" "+")
((((((((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Fiona is not kind.
False
9
inv-proof
[(((((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("Bob" "is" "smart" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Erin" "is" "round" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Bob" "is" "round" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is kind.[(triple1 OR ((((triple2 triple3) -> rule5)) -> rule7) OR ((((((triple3) -> rule1) triple3) -> rule5)) -> rule7))] Bob is quiet.[(triple2 OR ((triple3) -> rule1))] Bob is young.[(triple3)] Erin is kind.[(triple4 OR ((triple5) -> rule7))] Erin is rough.[(triple5)] Erin is smart.[(triple6)] Fiona is red.[(triple7)] Harry is not red.[(triple8)] Harry is round.[(triple9)] Harry is young.[(triple10 OR ((triple9) -> rule4))] @1: Bob is rough.[(((triple2 triple3) -> rule5) OR ((triple3 triple1) -> rule6) OR ((((triple3) -> rule1) triple3) -> rule5))] Erin is not quiet.[(((triple6) -> rule3))] Fiona is round.[(((triple7) -> rule9))] Harry is quiet.[(((triple10) -> rule1) OR ((((triple9) -> rule4)) -> rule1))] @2: Fiona is young.[(((((triple7) -> rule9)) -> rule4))] Harry is rough.[(((((triple10) -> rule1) triple10) -> rule5) OR ((((triple10) -> rule1) ((triple9) -> rule4)) -> rule5) OR ((((((triple9) -> rule4)) -> rule1) triple10) -> rule5) OR ((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule4)) -> rule5))] @3: Fiona is quiet.[(((((((triple7) -> rule9)) -> rule4)) -> rule1))] Harry is kind.[(((((((triple10) -> rule1) triple10) -> rule5)) -> rule7) OR ((((((triple10) -> rule1) ((triple9) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple9) -> rule4)) -> rule1) triple10) -> rule5)) -> rule7) OR ((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule4)) -> rule5)) -> rule7))] @4: Fiona is rough.[(((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5))] @5: Fiona is kind.[(((((((((((triple7) -> rule9)) -> rule4)) -> rule1) ((((triple7) -> rule9)) -> rule4)) -> rule5)) -> rule7))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((((triple2 triple3) -> (rule5 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple5) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Harry is not red.
("Harry" "is" "red" "-")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
((triple9) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2 triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 triple1) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple6) -> (rule3 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple7) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple7) -> (rule9 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple10) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2)) ((triple9) -> (rule4 % int3))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple7) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple10) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple10) -> (rule1 % int4)) ((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule1 % int3)) ((triple9) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple7) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple7) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5