Bob is big. Bob is rough. Bob is round. Bob is white. Charlie is nice. Charlie is rough. Charlie is white. Erin is cold. Gary is nice. Gary is rough. Nice, round people are big. White people are nice. If Charlie is rough then Charlie is cold. If Gary is white and Gary is cold then Gary is rough. If someone is red and nice then they are white. If Gary is rough and Gary is white then Gary is nice. If someone is nice then they are rough. Cold, round people are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Nice, round people are big.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is rough then Charlie is cold.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "cold" "+"))
If Gary is white and Gary is cold then Gary is rough.
((("Gary" "is" "white" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "+"))
If someone is red and nice then they are white.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Gary is rough and Gary is white then Gary is nice.
((("Gary" "is" "rough" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "nice" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Cold, round people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Gary is nice.
True
1
proof
[(triple9)]
("Gary" "is" "nice" "+")
triple9
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Charlie is cold.
True
2
proof
[(((triple6) -> rule3) OR ((((triple5) -> rule7)) -> rule3) OR ((((((triple7) -> rule2)) -> rule7)) -> rule3))]
("Charlie" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not cold.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple5) -> rule7)) -> rule3) OR ((((((triple7) -> rule2)) -> rule7)) -> rule3))]
("Charlie" "is" "cold" "-")
((triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is big.[(triple1 OR ((((triple4) -> rule2) triple3) -> rule1))] Bob is rough.[(triple2 OR ((((triple4) -> rule2)) -> rule7))] Bob is round.[(triple3)] Bob is white.[(triple4)] Charlie is nice.[(triple5 OR ((triple7) -> rule2))] Charlie is rough.[(triple6 OR ((triple5) -> rule7) OR ((((triple7) -> rule2)) -> rule7))] Charlie is white.[(triple7)] Erin is cold.[(triple8)] Gary is nice.[(triple9)] Gary is rough.[(triple10 OR ((triple9) -> rule7))] @1: Bob is nice.[(((triple4) -> rule2))] Charlie is cold.[(((triple6) -> rule3) OR ((((triple5) -> rule7)) -> rule3) OR ((((((triple7) -> rule2)) -> rule7)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple2
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple7) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple5) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple9) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3