Anne is big. Anne is green. Charlie is nice. Charlie is smart. Fiona is big. Gary is big. Gary is not cold. All big people are white. All cold people are green. If someone is nice and smart then they are green. All furry, big people are green. If Gary is cold and Gary is nice then Gary is not smart. If Gary is furry then Gary is big. If Fiona is big then Fiona is white. If someone is white and not cold then they are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and smart then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All furry, big people are green.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Gary is cold and Gary is nice then Gary is not smart.
((("Gary" "is" "cold" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "-"))
If Gary is furry then Gary is big.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "big" "+"))
If Fiona is big then Fiona is white.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "white" "+"))
If someone is white and not cold then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
Anne is green.
True
1
proof
[(triple2)]
("Anne" "is" "green" "+")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is not green.
False
3
inv-proof
[(((triple3 triple4) -> rule3))]
("Charlie" "is" "green" "-")
((triple3 triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is nice.
True
4
proof
[(((((triple6) -> rule1) triple7) -> rule8))]
("Gary" "is" "nice" "+")
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((((triple6) -> rule1) triple7) -> rule8))]
("Gary" "is" "nice" "-")
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "+")
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is smart.[(triple4)] Fiona is big.[(triple5)] Gary is big.[(triple6)] Gary is not cold.[(triple7)] @1: Anne is white.[(((triple1) -> rule1))] Charlie is green.[(((triple3 triple4) -> rule3))] Fiona is white.[(((triple5) -> rule1) OR ((triple5) -> rule7))] Gary is white.[(((triple6) -> rule1))] @2: Gary is nice.[(((((triple6) -> rule1) triple7) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3 triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple5) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple5) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple6) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2