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