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