Bob is not big. Bob is not red. Bob is round. Bob is not white. Fiona is kind. Fiona is round. Fiona is white. Harry is big. Harry is not kind. Harry is nice. Harry is red. Harry is not round. If someone is big then they are not kind. All kind, round people are white. If someone is kind and not red then they are not nice. Red people are big. If Bob is round then Bob is not white. Kind, white people are smart. If Fiona is smart then Fiona is nice. If Bob is smart and Bob is round then Bob is big.
Bob is not big.
("Bob" "is" "big" "-")
Bob is not red.
("Bob" "is" "red" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is not white.
("Bob" "is" "white" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not round.
("Harry" "is" "round" "-")
If someone is big then they are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
All kind, round people are white.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and not red then they are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "-"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Bob is round then Bob is not white.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "white" "-"))
Kind, white people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is smart then Fiona is nice.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "nice" "+"))
If Bob is smart and Bob is round then Bob is big.
((("Bob" "is" "smart" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "big" "+"))
Bob is not red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Fiona is smart.
True
3
proof
[(((triple5 triple7) -> rule6) OR ((triple5 ((triple5 triple6) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "+")
((triple5 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 ((triple5 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((triple5 triple7) -> rule6) OR ((triple5 ((triple5 triple6) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "-")
((triple5 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 ((triple5 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
True
4
proof
[(((((triple5 triple7) -> rule6)) -> rule7) OR ((((triple5 ((triple5 triple6) -> rule2)) -> rule6)) -> rule7))]
("Fiona" "is" "nice" "+")
((((triple5 triple7) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple5 ((triple5 triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not nice.
False
4
inv-proof
[(((((triple5 triple7) -> rule6)) -> rule7) OR ((((triple5 ((triple5 triple6) -> rule2)) -> rule6)) -> rule7))]
("Fiona" "is" "nice" "-")
((((triple5 triple7) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple5 ((triple5 triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "big" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is not big.[(triple1)] Bob is not red.[(triple2)] Bob is not white.[(triple4 OR ((triple3) -> rule5))] Bob is round.[(triple3)] Fiona is kind.[(triple5)] Fiona is round.[(triple6)] Fiona is white.[(triple7 OR ((triple5 triple6) -> rule2))] Harry is big.[(triple8 OR ((triple11) -> rule4))] Harry is nice.[(triple10)] Harry is not kind.[(triple9 OR ((triple8) -> rule1) OR ((((triple11) -> rule4)) -> rule1))] Harry is not round.[(triple12)] Harry is red.[(triple11)] @1: Fiona is smart.[(((triple5 triple7) -> rule6) OR ((triple5 ((triple5 triple6) -> rule2)) -> rule6))] @2: Fiona is nice.[(((((triple5 triple7) -> rule6)) -> rule7) OR ((((triple5 ((triple5 triple6) -> rule2)) -> rule6)) -> rule7))]
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple4
((triple3) -> (rule5 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((triple5 triple6) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple11) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
((triple8) -> (rule1 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple5 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 ((triple5 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple5 triple7) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple5 ((triple5 triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3