Bob is nice. Charlie is smart. Erin is big. Erin is cold. Erin is nice. Erin is round. Gary is green. Gary is nice. Gary is rough. Gary is smart. All round, big people are not rough. Smart, nice people are rough. All big people are green. Nice, green people are cold. If Gary is big and Gary is not smart then Gary is cold. If Charlie is smart then Charlie is nice. If someone is nice and rough then they are big. All green people are big.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All round, big people are not rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
Smart, nice people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Nice, green people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Gary is big and Gary is not smart then Gary is cold.
((("Gary" "is" "big" "+") ("Gary" "is" "smart" "~")) -> ("Gary" "is" "cold" "+"))
If Charlie is smart then Charlie is nice.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is nice and rough then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Erin is nice.
True
1
proof
[(triple5)]
("Erin" "is" "nice" "+")
triple5
Gary is not nice.
False
1
inv-proof
[(triple8)]
("Gary" "is" "nice" "-")
triple8
Erin is green.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple7) -> rule8) OR ((triple8 triple9) -> rule7) OR ((triple8 ((triple10 triple8) -> rule2)) -> rule7))]
("Gary" "is" "big" "-")
((triple7) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple8 triple9) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple8 ((triple10 triple8) -> (rule2 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is rough.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "rough" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
True
7
proof
[(((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int3)) ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not big.
False
7
inv-proof
[(((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule6 % int3)) ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is green.
True
8
proof
[(((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3))]
("Charlie" "is" "green" "+")
((((((triple2) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is not green.
False
8
inv-proof
[(((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3))]
("Charlie" "is" "green" "-")
((((((triple2) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is cold.
True
11
proof
[(((((triple2) -> rule6) ((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
("Charlie" "is" "cold" "+")
((((triple2) -> (rule6 % int5)) ((((((triple2) -> (rule6 % int5)) ((triple2 ((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Charlie is not cold.
False
11
inv-proof
[(((((triple2) -> rule6) ((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
("Charlie" "is" "cold" "-")
((((triple2) -> (rule6 % int5)) ((((((triple2) -> (rule6 % int5)) ((triple2 ((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is big.
Unknown
rconc
[@4: Bob is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule7 <- rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is nice.[(triple1)] Charlie is smart.[(triple2)] Erin is big.[(triple3)] Erin is cold.[(triple4 OR ((triple5 ((triple3) -> rule3)) -> rule4))] Erin is nice.[(triple5)] Erin is round.[(triple6)] Gary is green.[(triple7 OR ((((triple8 triple9) -> rule7)) -> rule3) OR ((((triple8 ((triple10 triple8) -> rule2)) -> rule7)) -> rule3))] Gary is nice.[(triple8)] Gary is rough.[(triple9 OR ((triple10 triple8) -> rule2))] Gary is smart.[(triple10)] @1: Charlie is nice.[(((triple2) -> rule6))] Erin is green.[(((triple3) -> rule3))] Erin is not rough.[(((triple6 triple3) -> rule1))] Gary is big.[(((triple7) -> rule8) OR ((triple8 triple9) -> rule7) OR ((triple8 ((triple10 triple8) -> rule2)) -> rule7))] Gary is cold.[(((triple8 triple7) -> rule4) OR ((triple8 ((((triple8 triple9) -> rule7)) -> rule3)) -> rule4) OR ((triple8 ((((triple8 ((triple10 triple8) -> rule2)) -> rule7)) -> rule3)) -> rule4))] @2: Charlie is rough.[(((triple2 ((triple2) -> rule6)) -> rule2))] @3: Charlie is big.[(((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7))] @4: Charlie is green.[(((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3))] @5: Charlie is cold.[(((((triple2) -> rule6) ((((((triple2) -> rule6) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((triple5 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((((triple8 triple9) -> (rule7 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple8 ((triple10 triple8) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple10 triple8) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((triple6 triple3) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple8 triple9) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple8 ((triple10 triple8) -> (rule2 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple8 triple7) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple8 ((((triple8 triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple8 ((((triple8 ((triple10 triple8) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int3)) ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple2) -> (rule6 % int4)) ((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule6 % int5)) ((((((triple2) -> (rule6 % int5)) ((triple2 ((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5