Charlie is cold. Erin is nice. Fiona is nice. Fiona is quiet. Gary is big. Gary is green. Gary is red. All nice, green things are quiet. Cold things are young. All cold things are green. All young, nice things are big. If Charlie is green then Charlie is quiet. If something is young then it is nice.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
All nice, green things are quiet.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All young, nice things are big.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Charlie is green then Charlie is quiet.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Fiona is not nice.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "nice" "-")
triple3
Charlie is young.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "-")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Charlie is cold.[(triple1)] Erin is nice.[(triple2)] Fiona is nice.[(triple3)] Fiona is quiet.[(triple4)] Gary is big.[(triple5)] Gary is green.[(triple6)] Gary is red.[(triple7)] @1: Charlie is green.[(((triple1) -> rule3))] Charlie is young.[(((triple1) -> rule2))] @2: Charlie is nice.[(((((triple1) -> rule2)) -> rule6))] Charlie is quiet.[(((((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule1))] @3: Charlie is big.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule6)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3