Bob is big. Bob is kind. Bob is red. Bob is rough. Bob is white. Erin is big. Erin is kind. Fiona is not red. Fiona is rough. Fiona is not round. Gary is rough. All smart people are round. All white, smart people are big. If Gary is white then Gary is not smart. All big, round people are red. White people are rough. Round, red people are white. All kind, big people are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is rough.
("Gary" "is" "rough" "+")
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All white, smart people are big.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Gary is white then Gary is not smart.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "-"))
All big, round people are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Round, red people are white.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All kind, big people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Fiona is not rough.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "rough" "-")
triple9
Erin is smart.
True
3
proof
[(((triple7 triple6) -> rule7))]
("Erin" "is" "smart" "+")
((triple7 triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not smart.
False
3
inv-proof
[(((triple2 triple1) -> rule7))]
("Bob" "is" "smart" "-")
((triple2 triple1) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
True
4
proof
[(((((triple2 triple1) -> rule7)) -> rule1))]
("Bob" "is" "round" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is not round.
False
4
inv-proof
[(((((triple7 triple6) -> rule7)) -> rule1))]
("Erin" "is" "round" "-")
((((triple7 triple6) -> (rule7 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
True
6
proof
[(((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4))]
("Erin" "is" "red" "+")
((triple6 ((((triple7 triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not red.
False
6
inv-proof
[(((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4))]
("Erin" "is" "red" "-")
((triple6 ((((triple7 triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
True
11
proof
[(((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6))]
("Erin" "is" "white" "+")
((((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3)) ((triple6 ((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not white.
False
11
inv-proof
[(((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6))]
("Erin" "is" "white" "-")
((((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3)) ((triple6 ((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is rough.
True
12
proof
[(((((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "rough" "+")
((((((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4)) ((triple6 ((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Erin is not rough.
False
12
inv-proof
[(((((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "rough" "-")
((((((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4)) ((triple6 ((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is white.
Unknown
rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "big" "-")
Gary is round.
Unknown
rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Gary" "is" "round" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is red.[(triple3 OR ((triple1 ((((triple2 triple1) -> rule7)) -> rule1)) -> rule4))] Bob is rough.[(triple4 OR ((triple5) -> rule5) OR ((((((((triple2 triple1) -> rule7)) -> rule1) triple3) -> rule6)) -> rule5) OR ((((((((triple2 triple1) -> rule7)) -> rule1) ((triple1 ((((triple2 triple1) -> rule7)) -> rule1)) -> rule4)) -> rule6)) -> rule5))] Bob is white.[(triple5 OR ((((((triple2 triple1) -> rule7)) -> rule1) triple3) -> rule6) OR ((((((triple2 triple1) -> rule7)) -> rule1) ((triple1 ((((triple2 triple1) -> rule7)) -> rule1)) -> rule4)) -> rule6))] Erin is big.[(triple6)] Erin is kind.[(triple7)] Fiona is not red.[(triple8)] Fiona is not round.[(triple10)] Fiona is rough.[(triple9)] Gary is rough.[(triple11)] @1: Bob is smart.[(((triple2 triple1) -> rule7))] Erin is smart.[(((triple7 triple6) -> rule7))] @2: Bob is round.[(((((triple2 triple1) -> rule7)) -> rule1))] Erin is round.[(((((triple7 triple6) -> rule7)) -> rule1))] @3: Erin is red.[(((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4))] @4: Erin is white.[(((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6))] @5: Erin is rough.[(((((((((triple7 triple6) -> rule7)) -> rule1) ((triple6 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule4)) -> rule6)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple1 ((((triple2 triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple5) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((((((triple2 triple1) -> (rule7 % int4))) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((((triple2 triple1) -> (rule7 % int5))) -> (rule1 % int4)) ((triple1 ((((triple2 triple1) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
triple5
((((((triple2 triple1) -> (rule7 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple2 triple1) -> (rule7 % int4))) -> (rule1 % int3)) ((triple1 ((((triple2 triple1) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Fiona is not red.
("Fiona" "is" "red" "-")
triple8
Fiona is not round.
("Fiona" "is" "round" "-")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple1) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7 triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple7 triple6) -> (rule7 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple6 ((((triple7 triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3)) ((triple6 ((((triple7 triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
((((((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4)) ((triple6 ((((triple7 triple6) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5