Bob is blue. Bob is green. Bob is nice. Charlie is big. Dave is big. Dave is blue. Dave is cold. Dave is green. Dave is not nice. Dave is not red. Dave is white. Gary is green. Gary is nice. Gary is red. Gary is white. If Charlie is blue and Charlie is not red then Charlie is not white. If Charlie is green then Charlie is nice. Big things are white. All big, blue things are green. If something is white then it is green. If Dave is white and Dave is not blue then Dave is red. If something is cold and white then it is big. If something is white and not green then it is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is white.
("Dave" "is" "white" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If Charlie is blue and Charlie is not red then Charlie is not white.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "red" "~")) -> ("Charlie" "is" "white" "-"))
If Charlie is green then Charlie is nice.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "nice" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All big, blue things are green.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is white then it is green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Dave is white and Dave is not blue then Dave is red.
((("Dave" "is" "white" "+") ("Dave" "is" "blue" "~")) -> ("Dave" "is" "red" "+"))
If something is cold and white then it is big.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is white and not green then it is nice.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "nice" "+"))
Dave is green.
True
1
proof
[(triple8 OR ((triple11) -> rule5) OR ((triple5 triple6) -> rule4) OR ((((triple5) -> rule3)) -> rule5) OR ((((triple7 triple11) -> rule7) triple6) -> rule4))]
("Dave" "is" "green" "+")
triple8
((triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple7 triple11) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not green.
False
1
inv-proof
[(triple8 OR ((triple11) -> rule5) OR ((triple5 triple6) -> rule4) OR ((((triple5) -> rule3)) -> rule5) OR ((((triple7 triple11) -> rule7) triple6) -> rule4))]
("Dave" "is" "green" "-")
triple8
((triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple7 triple11) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is white.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "white" "+")
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "white" "-")
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Charlie" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Charlie" "is" "green" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not nice.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Bob" "is" "white" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Charlie is big.[(triple4)] Dave is big.[(triple5 OR ((triple7 triple11) -> rule7))] Dave is blue.[(triple6)] Dave is cold.[(triple7)] Dave is green.[(triple8 OR ((triple11) -> rule5) OR ((triple5 triple6) -> rule4) OR ((((triple5) -> rule3)) -> rule5) OR ((((triple7 triple11) -> rule7) triple6) -> rule4))] Dave is not nice.[(triple9)] Dave is not red.[(triple10)] Dave is white.[(triple11 OR ((triple5) -> rule3))] Gary is green.[(triple12 OR ((triple15) -> rule5))] Gary is nice.[(triple13)] Gary is red.[(triple14)] Gary is white.[(triple15)] @1: Charlie is white.[(((triple4) -> rule3))] @2: Charlie is green.[(((((triple4) -> rule3)) -> rule5))] @3: Charlie is nice.[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple7 triple11) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
((triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple7 triple11) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
triple9
Dave is not red.
("Dave" "is" "red" "-")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple5) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple12
((triple15) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3