Charlie is not big. Charlie is blue. Charlie is quiet. Charlie is not rough. Dave is green. Dave is quiet. Erin is big. Erin is blue. Erin is quiet. Harry is big. Harry is green. Harry is rough. If Harry is blue and Harry is red then Harry is kind. Green, red things are blue. Big, green things are red. If something is big then it is quiet. All rough, big things are quiet. If Charlie is red and Charlie is not kind then Charlie is blue.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is blue and Harry is red then Harry is kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
Green, red things are blue.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Big, green things are red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All rough, big things are quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is red and Charlie is not kind then Charlie is blue.
((("Charlie" "is" "red" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "blue" "+"))
Harry is big.
True
1
proof
[(triple10)]
("Harry" "is" "big" "+")
triple10
Erin is not big.
False
1
inv-proof
[(triple7)]
("Erin" "is" "big" "-")
triple7
Harry is quiet.
True
2
proof
[(((triple10) -> rule4) OR ((triple12 triple10) -> rule5))]
("Harry" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12 triple10) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple10 triple11) -> rule3))]
("Harry" "is" "red" "-")
((triple10 triple11) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
True
5
proof
[(((triple11 ((triple10 triple11) -> rule3)) -> rule2))]
("Harry" "is" "blue" "+")
((triple11 ((triple10 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not blue.
False
5
inv-proof
[(((triple11 ((triple10 triple11) -> rule3)) -> rule2))]
("Harry" "is" "blue" "-")
((triple11 ((triple10 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
True
9
proof
[(((((triple11 ((triple10 triple11) -> rule3)) -> rule2) ((triple10 triple11) -> rule3)) -> rule1))]
("Harry" "is" "kind" "+")
((((triple11 ((triple10 triple11) -> (rule3 % int3))) -> (rule2 % int2)) ((triple10 triple11) -> (rule3 % int3))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not kind.
False
9
inv-proof
[(((((triple11 ((triple10 triple11) -> rule3)) -> rule2) ((triple10 triple11) -> rule3)) -> rule1))]
("Harry" "is" "kind" "-")
((((triple11 ((triple10 triple11) -> (rule3 % int3))) -> (rule2 % int2)) ((triple10 triple11) -> (rule3 % int3))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is blue.[(triple2)] Charlie is not big.[(triple1)] Charlie is not rough.[(triple4)] Charlie is quiet.[(triple3)] Dave is green.[(triple5)] Dave is quiet.[(triple6)] Erin is big.[(triple7)] Erin is blue.[(triple8)] Erin is quiet.[(triple9 OR ((triple7) -> rule4))] Harry is big.[(triple10)] Harry is green.[(triple11)] Harry is rough.[(triple12)] @1: Harry is quiet.[(((triple10) -> rule4) OR ((triple12 triple10) -> rule5))] Harry is red.[(((triple10 triple11) -> rule3))] @2: Harry is blue.[(((triple11 ((triple10 triple11) -> rule3)) -> rule2))] @3: Harry is kind.[(((((triple11 ((triple10 triple11) -> rule3)) -> rule2) ((triple10 triple11) -> rule3)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple7) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple12 triple10) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple10 triple11) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple11 ((triple10 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple11 ((triple10 triple11) -> (rule3 % int3))) -> (rule2 % int2)) ((triple10 triple11) -> (rule3 % int3))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3