Charlie is rough. Dave is cold. Dave is nice. Dave is rough. Erin is cold. Erin is green. Erin is young. All rough, cold things are quiet. All nice things are cold. All rough things are nice.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
All rough, cold things are quiet.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Erin is green.
True
1
proof
[(triple6)]
("Erin" "is" "green" "+")
triple6
Erin is not cold.
False
1
inv-proof
[(triple5)]
("Erin" "is" "cold" "-")
triple5
Charlie is nice.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not quiet.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Charlie is rough.[(triple1)] Dave is cold.[(triple2 OR ((triple3) -> rule2) OR ((((triple4) -> rule3)) -> rule2))] Dave is nice.[(triple3 OR ((triple4) -> rule3))] Dave is rough.[(triple4)] Erin is cold.[(triple5)] Erin is green.[(triple6)] Erin is young.[(triple7)] @1: Charlie is nice.[(((triple1) -> rule3))] Dave is quiet.[(((triple4 triple2) -> rule1) OR ((triple4 ((triple3) -> rule2)) -> rule1) OR ((triple4 ((((triple4) -> rule3)) -> rule2)) -> rule1))] @2: Charlie is cold.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is quiet.[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule1))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4 triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple4 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3