Charlie is not green. Dave is red. Erin is smart. Fiona is nice. All big people are smart. If Fiona is not green and Fiona is not red then Fiona is big. If someone is smart then they are nice. All kind people are nice. Big people are not round. Red people are big. If Erin is not round then Erin is green. If Fiona is not round then Fiona is nice.
Charlie is not green.
("Charlie" "is" "green" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is not green and Fiona is not red then Fiona is big.
((("Fiona" "is" "green" "~") ("Fiona" "is" "red" "~")) -> ("Fiona" "is" "big" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Big people are not round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "-"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Erin is not round then Erin is green.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "green" "+"))
If Fiona is not round then Fiona is nice.
((("Fiona" "is" "round" "~")) -> ("Fiona" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple4)]
("Fiona" "is" "nice" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is big.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "big" "+")
((triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "big" "-")
((triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not round.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("Dave" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule5))]
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "-")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Charlie is not green.[(triple1)] Dave is red.[(triple2)] Erin is smart.[(triple3)] Fiona is nice.[(triple4)] @1: Dave is big.[(((triple2) -> rule6))] Erin is nice.[(((triple3) -> rule3))] @2: Dave is not round.[(((((triple2) -> rule6)) -> rule5))] Dave is smart.[(((((triple2) -> rule6)) -> rule1))] @3: Dave is nice.[(((((((triple2) -> rule6)) -> rule1)) -> rule3))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3