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