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