Bob is green. Bob is kind. Bob is not nice. Bob is smart. Bob is white. Charlie is quiet. Erin is nice. Erin is white. Fiona is green. Fiona is kind. Round, quiet things are smart. Round things are smart. If something is quiet then it is smart. If Charlie is round and Charlie is not kind then Charlie is not green. All green things are quiet. Round, smart things are nice. If Fiona is smart then Fiona is round. Round, nice things are not white. If Bob is nice and Bob is not kind then Bob is not quiet.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Round, quiet things are smart.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If Charlie is round and Charlie is not kind then Charlie is not green.
((("Charlie" "is" "round" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "green" "-"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Round, smart things are nice.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Fiona is smart then Fiona is round.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "round" "+"))
Round, nice things are not white.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "-"))
If Bob is nice and Bob is not kind then Bob is not quiet.
((("Bob" "is" "nice" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "quiet" "-"))
Bob is not nice.
True
1
proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Fiona is not kind.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "kind" "-")
triple10
Charlie is smart.
True
2
proof
[(((triple6) -> rule3))]
("Charlie" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple9) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "+")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "-")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
True
4
proof
[(((((((triple9) -> rule5)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "+")
((((((triple9) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not round.
False
4
inv-proof
[(((((((triple9) -> rule5)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "-")
((((((triple9) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
True
8
proof
[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "+")
((((((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not nice.
False
8
inv-proof
[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "-")
((((((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not white.
True
13
proof
[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6)) -> rule8))]
("Fiona" "is" "white" "-")
((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Fiona is white.
False
13
inv-proof
[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6)) -> rule8))]
("Fiona" "is" "white" "+")
((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is not nice.[(triple3)] Bob is smart.[(triple4 OR ((((triple1) -> rule5)) -> rule3))] Bob is white.[(triple5)] Charlie is quiet.[(triple6)] Erin is nice.[(triple7)] Erin is white.[(triple8)] Fiona is green.[(triple9)] Fiona is kind.[(triple10)] @1: Bob is quiet.[(((triple1) -> rule5))] Charlie is smart.[(((triple6) -> rule3))] Fiona is quiet.[(((triple9) -> rule5))] @2: Fiona is smart.[(((((triple9) -> rule5)) -> rule3))] @3: Fiona is round.[(((((((triple9) -> rule5)) -> rule3)) -> rule7))] @4: Fiona is nice.[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6))] @5: Fiona is not white.[(((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((((((triple9) -> rule5)) -> rule3)) -> rule7) ((((triple9) -> rule5)) -> rule3)) -> rule6)) -> rule8))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple9) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple9) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not white.
("Fiona" "is" "white" "-")
((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple9) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5