Charlie is big. Charlie is cold. Charlie is quiet. Charlie is rough. Charlie is young. Erin is young. Fiona is nice. Quiet things are rough. If Fiona is white then Fiona is big. If something is big then it is white. If something is big then it is quiet. All young things are cold. If something is white and not young then it is big. All quiet things are big. If Charlie is cold then Charlie is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If Fiona is white then Fiona is big.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "big" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is white and not young then it is big.
((("something" "is" "white" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Charlie is cold then Charlie is nice.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple7)]
("Fiona" "is" "nice" "+")
triple7
Charlie is not cold.
False
1
inv-proof
[(triple2 OR ((triple5) -> rule5))]
("Charlie" "is" "cold" "-")
triple2
((triple5) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
True
2
proof
[(((triple2) -> rule8) OR ((((triple5) -> rule5)) -> rule8))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple3) -> rule7)) -> rule3))]
("Charlie" "is" "white" "-")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@5: Fiona is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule7 <- rule4 <- rule6 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is white.
Unknown
rconc
[@4: Fiona is white.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "white" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is big.[(triple1 OR ((triple3) -> rule7))] Charlie is cold.[(triple2 OR ((triple5) -> rule5))] Charlie is quiet.[(triple3 OR ((triple1) -> rule4))] Charlie is rough.[(triple4 OR ((triple3) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] Charlie is young.[(triple5)] Erin is young.[(triple6)] Fiona is nice.[(triple7)] @1: Charlie is nice.[(((triple2) -> rule8) OR ((((triple5) -> rule5)) -> rule8))] Charlie is white.[(((triple1) -> rule3) OR ((((triple3) -> rule7)) -> rule3))] Erin is cold.[(((triple6) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple5) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple6) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1