Charlie is blue. Charlie is rough. Charlie is round. Erin is cold. Erin is nice. Erin is rough. Erin is round. Erin is white. Erin is young. Harry is cold. Harry is nice. Harry is white. If Harry is blue and Harry is rough then Harry is round. If Erin is white then Erin is nice. If Harry is rough then Harry is young. Young, white people are cold. If someone is round and blue then they are cold. If someone is nice then they are rough. Blue people are white. If someone is round then they are cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is blue and Harry is rough then Harry is round.
((("Harry" "is" "blue" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
If Erin is white then Erin is nice.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "nice" "+"))
If Harry is rough then Harry is young.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "young" "+"))
Young, white people are cold.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and blue then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule6) OR ((((triple8) -> rule2)) -> rule6))]
("Erin" "is" "rough" "-")
triple6
((triple5) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Charlie is cold.
True
2
proof
[(((triple3) -> rule8) OR ((triple3 triple1) -> rule5))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple3 triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "white" "-")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is young.
True
3
proof
[(((((triple11) -> rule6)) -> rule3))]
("Harry" "is" "young" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule3))]
("Harry" "is" "young" "-")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is rough.[(triple2)] Charlie is round.[(triple3)] Erin is cold.[(triple4 OR ((triple7) -> rule8) OR ((triple9 triple8) -> rule4))] Erin is nice.[(triple5 OR ((triple8) -> rule2))] Erin is rough.[(triple6 OR ((triple5) -> rule6) OR ((((triple8) -> rule2)) -> rule6))] Erin is round.[(triple7)] Erin is white.[(triple8)] Erin is young.[(triple9)] Harry is cold.[(triple10 OR ((((((triple11) -> rule6)) -> rule3) triple12) -> rule4))] Harry is nice.[(triple11)] Harry is white.[(triple12)] @1: Charlie is cold.[(((triple3) -> rule8) OR ((triple3 triple1) -> rule5))] Charlie is white.[(((triple1) -> rule7))] Harry is rough.[(((triple11) -> rule6))] @2: Harry is young.[(((((triple11) -> rule6)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((triple7) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple9 triple8) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((triple8) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple5) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple3 triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple11) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2