Bob is not kind. Charlie is nice. Charlie is red. Charlie is smart. Dave is blue. Fiona is green. Fiona is smart. If someone is nice and rough then they are not green. If Charlie is red then Charlie is smart. All blue people are rough. If Bob is green then Bob is not blue. Smart, nice people are blue. If someone is kind and smart then they are nice.
Bob is not kind.
("Bob" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is nice and rough then they are not green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If Charlie is red then Charlie is smart.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "smart" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Bob is green then Bob is not blue.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "blue" "-"))
Smart, nice people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and smart then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Charlie is red.
True
1
proof
[(triple3)]
("Charlie" "is" "red" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule2))]
("Charlie" "is" "smart" "-")
triple4
((triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is rough.
True
2
proof
[(((triple5) -> rule3))]
("Dave" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not blue.
False
3
inv-proof
[(((triple4 triple2) -> rule5) OR ((((triple3) -> rule2) triple2) -> rule5))]
("Charlie" "is" "blue" "-")
((triple4 triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
True
4
proof
[(((((triple4 triple2) -> rule5)) -> rule3) OR ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple4 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((((triple4 triple2) -> rule5)) -> rule3) OR ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3))]
("Charlie" "is" "rough" "-")
((((triple4 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not green.
True
6
proof
[(((triple2 ((((triple4 triple2) -> rule5)) -> rule3)) -> rule1) OR ((triple2 ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3)) -> rule1))]
("Charlie" "is" "green" "-")
((triple2 ((((triple4 triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple2 ((((((triple3) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is green.
False
6
inv-proof
[(((triple2 ((((triple4 triple2) -> rule5)) -> rule3)) -> rule1) OR ((triple2 ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3)) -> rule1))]
("Charlie" "is" "green" "+")
((triple2 ((((triple4 triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple2 ((((((triple3) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is not kind.[(triple1)] Charlie is nice.[(triple2)] Charlie is red.[(triple3)] Charlie is smart.[(triple4 OR ((triple3) -> rule2))] Dave is blue.[(triple5)] Fiona is green.[(triple6)] Fiona is smart.[(triple7)] @1: Charlie is blue.[(((triple4 triple2) -> rule5) OR ((((triple3) -> rule2) triple2) -> rule5))] Dave is rough.[(((triple5) -> rule3))] @2: Charlie is rough.[(((((triple4 triple2) -> rule5)) -> rule3) OR ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3))] @3: Charlie is not green.[(((triple2 ((((triple4 triple2) -> rule5)) -> rule3)) -> rule1) OR ((triple2 ((((((triple3) -> rule2) triple2) -> rule5)) -> rule3)) -> rule1))]
Bob is not kind.
("Bob" "is" "kind" "-")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4 triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple4 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not green.
("Charlie" "is" "green" "-")
((triple2 ((((triple4 triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple2 ((((((triple3) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4