Bob is quiet. Erin is rough. Erin is smart. Harry is nice. Harry is quiet. Harry is smart. Harry is white. If someone is quiet then they are rough. Rough, nice people are red. If Erin is quiet and Erin is rough then Erin is smart. If Bob is big then Bob is white. All quiet, smart people are nice. If someone is white and big then they are red.
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Rough, nice people are red.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Erin is quiet and Erin is rough then Erin is smart.
((("Erin" "is" "quiet" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
If Bob is big then Bob is white.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "+"))
All quiet, smart people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and big then they are red.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Harry is smart.
True
1
proof
[(triple6)]
("Harry" "is" "smart" "+")
triple6
Erin is not rough.
False
1
inv-proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Harry is rough.
True
2
proof
[(((triple5) -> rule1))]
("Harry" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Harry" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
True
4
proof
[(((((triple5) -> rule1) triple4) -> rule2) OR ((((triple5) -> rule1) ((triple5 triple6) -> rule5)) -> rule2))]
("Harry" "is" "red" "+")
((((triple5) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple5 triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not red.
False
4
inv-proof
[(((((triple5) -> rule1) triple4) -> rule2) OR ((((triple5) -> rule1) ((triple5 triple6) -> rule5)) -> rule2))]
("Harry" "is" "red" "-")
((((triple5) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple5 triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "red" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "red" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Bob is quiet.[(triple1)] Erin is rough.[(triple2)] Erin is smart.[(triple3)] Harry is nice.[(triple4 OR ((triple5 triple6) -> rule5))] Harry is quiet.[(triple5)] Harry is smart.[(triple6)] Harry is white.[(triple7)] @1: Bob is rough.[(((triple1) -> rule1))] Harry is rough.[(((triple5) -> rule1))] @2: Harry is red.[(((((triple5) -> rule1) triple4) -> rule2) OR ((((triple5) -> rule1) ((triple5 triple6) -> rule5)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
((triple5 triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple5) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple5 triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3