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