Bob is red. Bob is rough. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is white. Fiona is blue. Fiona is quiet. Fiona is rough. Harry is rough. If someone is blue and furry then they are rough. If Harry is blue and Harry is furry then Harry is red. If someone is blue and white then they are kind. If someone is kind then they are furry. All rough people are kind. All furry, kind people are red.
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is blue and furry then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Harry is blue and Harry is furry then Harry is red.
((("Harry" "is" "blue" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "red" "+"))
If someone is blue and white then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All furry, kind people are red.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple5) -> rule5))]
("Charlie" "is" "kind" "+")
triple3
((triple5) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple3 OR ((triple5) -> rule5))]
("Charlie" "is" "kind" "-")
triple3
((triple5) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is kind.
True
2
proof
[(((triple9) -> rule5))]
("Fiona" "is" "kind" "+")
((triple9) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((triple5) -> rule5)) -> rule4))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule6) OR ((((triple3) -> rule4) ((triple5) -> rule5)) -> rule6) OR ((((((triple5) -> rule5)) -> rule4) triple3) -> rule6) OR ((((((triple5) -> rule5)) -> rule4) ((triple5) -> rule5)) -> rule6))]
("Charlie" "is" "red" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) ((triple5) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is not furry.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule4))]
("Fiona" "is" "furry" "-")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
True
6
proof
[(((((((triple9) -> rule5)) -> rule4) ((triple9) -> rule5)) -> rule6))]
("Fiona" "is" "red" "+")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not red.
False
6
inv-proof
[(((((((triple9) -> rule5)) -> rule4) ((triple9) -> rule5)) -> rule6))]
("Fiona" "is" "red" "-")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Bob is red.[(triple1 OR ((((((triple2) -> rule5)) -> rule4) ((triple2) -> rule5)) -> rule6))] Bob is rough.[(triple2)] Charlie is kind.[(triple3 OR ((triple5) -> rule5))] Charlie is quiet.[(triple4)] Charlie is rough.[(triple5)] Charlie is white.[(triple6)] Fiona is blue.[(triple7)] Fiona is quiet.[(triple8)] Fiona is rough.[(triple9)] Harry is rough.[(triple10)] @1: Bob is kind.[(((triple2) -> rule5))] Charlie is furry.[(((triple3) -> rule4) OR ((((triple5) -> rule5)) -> rule4))] Fiona is kind.[(((triple9) -> rule5))] Harry is kind.[(((triple10) -> rule5))] @2: Bob is furry.[(((((triple2) -> rule5)) -> rule4))] Charlie is red.[(((((triple3) -> rule4) triple3) -> rule6) OR ((((triple3) -> rule4) ((triple5) -> rule5)) -> rule6) OR ((((((triple5) -> rule5)) -> rule4) triple3) -> rule6) OR ((((((triple5) -> rule5)) -> rule4) ((triple5) -> rule5)) -> rule6))] Fiona is furry.[(((((triple9) -> rule5)) -> rule4))] Harry is furry.[(((((triple10) -> rule5)) -> rule4))] @3: Fiona is red.[(((((((triple9) -> rule5)) -> rule4) ((triple9) -> rule5)) -> rule6))] Harry is red.[(((((((triple10) -> rule5)) -> rule4) ((triple10) -> rule5)) -> rule6))]
Bob is red.
("Bob" "is" "red" "+")
triple1
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2) -> (rule5 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple5) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) ((triple5) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2)) ((triple10) -> (rule5 % int3))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3