Bob is blue. Bob is nice. Bob is round. Bob is white. Charlie is blue. Charlie is red. Fiona is blue. Fiona is rough. Gary is not red. Gary is rough. If Charlie is not nice and Charlie is not blue then Charlie is red. If Charlie is white then Charlie is red. If Fiona is round then Fiona is not nice. All rough things are white. If something is red and big then it is white. Big, blue things are round. White, blue things are red. Nice, white things are red. If something is rough and red then it is big.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is rough.
("Gary" "is" "rough" "+")
If Charlie is not nice and Charlie is not blue then Charlie is red.
((("Charlie" "is" "nice" "~") ("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "red" "+"))
If Charlie is white then Charlie is red.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "red" "+"))
If Fiona is round then Fiona is not nice.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "nice" "-"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is red and big then it is white.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Big, blue things are round.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
White, blue things are red.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Nice, white things are red.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is rough and red then it is big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Gary is rough.
True
1
proof
[(triple10)]
("Gary" "is" "rough" "+")
triple10
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Bob is red.
True
3
proof
[(((triple2 triple4) -> rule8) OR ((triple4 triple1) -> rule7))]
("Bob" "is" "red" "+")
((triple2 triple4) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple4 triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
3
inv-proof
[(((triple2 triple4) -> rule8) OR ((triple4 triple1) -> rule7))]
("Bob" "is" "red" "-")
((triple2 triple4) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple4 triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is red.
True
4
proof
[(((((triple8) -> rule4) triple7) -> rule7))]
("Fiona" "is" "red" "+")
((((triple8) -> (rule4 % int2)) triple7) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not red.
False
4
inv-proof
[(((((triple8) -> rule4) triple7) -> rule7))]
("Fiona" "is" "red" "-")
((((triple8) -> (rule4 % int2)) triple7) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
True
6
proof
[(((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9))]
("Fiona" "is" "big" "+")
((triple8 ((((triple8) -> (rule4 % int3)) triple7) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not big.
False
6
inv-proof
[(((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9))]
("Fiona" "is" "big" "-")
((triple8 ((((triple8) -> (rule4 % int3)) triple7) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is round.
True
8
proof
[(((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6))]
("Fiona" "is" "round" "+")
((((triple8 ((((triple8) -> (rule4 % int4)) triple7) -> (rule7 % int3))) -> (rule9 % int2)) triple7) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not round.
False
8
inv-proof
[(((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6))]
("Fiona" "is" "round" "-")
((((triple8 ((((triple8) -> (rule4 % int4)) triple7) -> (rule7 % int3))) -> (rule9 % int2)) triple7) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not nice.
True
9
proof
[(((((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6)) -> rule3))]
("Fiona" "is" "nice" "-")
((((((triple8 ((((triple8) -> (rule4 % int5)) triple7) -> (rule7 % int4))) -> (rule9 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Fiona is nice.
False
9
inv-proof
[(((((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6)) -> rule3))]
("Fiona" "is" "nice" "+")
((((((triple8 ((((triple8) -> (rule4 % int5)) triple7) -> (rule7 % int4))) -> (rule9 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Bob" "is" "big" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Gary" "is" "big" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule9 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule5 <- rule9 <- FAIL)]]
("Charlie" "is" "white" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4)] Charlie is blue.[(triple5)] Charlie is red.[(triple6)] Fiona is blue.[(triple7)] Fiona is rough.[(triple8)] Gary is not red.[(triple9)] Gary is rough.[(triple10)] @1: Bob is red.[(((triple2 triple4) -> rule8) OR ((triple4 triple1) -> rule7))] Fiona is white.[(((triple8) -> rule4))] Gary is white.[(((triple10) -> rule4))] @2: Fiona is red.[(((((triple8) -> rule4) triple7) -> rule7))] @3: Fiona is big.[(((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9))] @4: Fiona is round.[(((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6))] @5: Fiona is not nice.[(((((((triple8 ((((triple8) -> rule4) triple7) -> rule7)) -> rule9) triple7) -> rule6)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Gary is not red.
("Gary" "is" "red" "-")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple2 triple4) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple4 triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple8) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple10) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple8) -> (rule4 % int2)) triple7) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple8 ((((triple8) -> (rule4 % int3)) triple7) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((triple8 ((((triple8) -> (rule4 % int4)) triple7) -> (rule7 % int3))) -> (rule9 % int2)) triple7) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((((triple8 ((((triple8) -> (rule4 % int5)) triple7) -> (rule7 % int4))) -> (rule9 % int3)) triple7) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5