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