Charlie is green. Dave is green. Erin is nice. Harry is nice. All cold people are young. If someone is cold and young then they are rough. White people are young. Nice people are cold. All young people are green. Cold people are red. If someone is white and rough then they are cold. Nice people are white.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and young then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is white and rough then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Harry is white.
True
2
proof
[(((triple4) -> rule8))]
("Harry" "is" "white" "+")
((triple4) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple3) -> rule8))]
("Erin" "is" "white" "-")
((triple3) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is red.
True
3
proof
[(((((triple4) -> rule4)) -> rule6))]
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1) OR ((((triple3) -> rule8)) -> rule3))]
("Erin" "is" "young" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
True
6
proof
[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule1)) -> rule2) OR ((((triple3) -> rule4) ((((triple3) -> rule8)) -> rule3)) -> rule2))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Harry is not green.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule1)) -> rule5) OR ((((((triple4) -> rule8)) -> rule3)) -> rule5))]
("Harry" "is" "green" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule8 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is green.[(triple1)] Dave is green.[(triple2)] Erin is nice.[(triple3)] Harry is nice.[(triple4)] @1: Erin is cold.[(((triple3) -> rule4))] Erin is white.[(((triple3) -> rule8))] Harry is cold.[(((triple4) -> rule4))] Harry is white.[(((triple4) -> rule8))] @2: Erin is red.[(((((triple3) -> rule4)) -> rule6))] Erin is young.[(((((triple3) -> rule4)) -> rule1) OR ((((triple3) -> rule8)) -> rule3))] Harry is red.[(((((triple4) -> rule4)) -> rule6))] Harry is young.[(((((triple4) -> rule4)) -> rule1) OR ((((triple4) -> rule8)) -> rule3))] @3: Erin is green.[(((((((triple3) -> rule4)) -> rule1)) -> rule5) OR ((((((triple3) -> rule8)) -> rule3)) -> rule5))] Erin is rough.[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule1)) -> rule2) OR ((((triple3) -> rule4) ((((triple3) -> rule8)) -> rule3)) -> rule2))] Harry is green.[(((((((triple4) -> rule4)) -> rule1)) -> rule5) OR ((((((triple4) -> rule8)) -> rule3)) -> rule5))] Harry is rough.[(((((triple4) -> rule4) ((((triple4) -> rule4)) -> rule1)) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule8)) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4