Fiona is kind. Fiona is nice. Fiona is quiet. Fiona is red. Harry is kind. Harry is rough. Harry is smart. If someone is cold then they are smart. Nice, smart people are quiet. Kind people are cold. Smart people are rough. Smart people are kind. Nice, quiet people are kind.
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Nice, smart people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Nice, quiet people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple5 OR ((triple7) -> rule5))]
("Harry" "is" "kind" "+")
triple5
((triple7) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Fiona is not red.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "red" "-")
triple4
Harry is cold.
True
2
proof
[(((triple5) -> rule3) OR ((((triple7) -> rule5)) -> rule3))]
("Harry" "is" "cold" "+")
((triple5) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Fiona is not cold.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2 triple3) -> rule6)) -> rule3))]
("Fiona" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple2 triple3) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1))]
("Fiona" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple2 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1))]
("Fiona" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple2 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4) OR ((((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1)) -> rule4))]
("Fiona" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((((triple2 triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is not rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4) OR ((((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1)) -> rule4))]
("Fiona" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((((triple2 triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Fiona is kind.[(triple1 OR ((triple2 triple3) -> rule6))] Fiona is nice.[(triple2)] Fiona is quiet.[(triple3 OR ((triple2 ((((triple1) -> rule3)) -> rule1)) -> rule2))] Fiona is red.[(triple4)] Harry is kind.[(triple5 OR ((triple7) -> rule5))] Harry is rough.[(triple6 OR ((triple7) -> rule4) OR ((((((triple5) -> rule3)) -> rule1)) -> rule4))] Harry is smart.[(triple7 OR ((((triple5) -> rule3)) -> rule1))] @1: Fiona is cold.[(((triple1) -> rule3) OR ((((triple2 triple3) -> rule6)) -> rule3))] Harry is cold.[(((triple5) -> rule3) OR ((((triple7) -> rule5)) -> rule3))] @2: Fiona is smart.[(((((triple1) -> rule3)) -> rule1) OR ((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1))] @3: Fiona is rough.[(((((((triple1) -> rule3)) -> rule1)) -> rule4) OR ((((((((triple2 triple3) -> rule6)) -> rule3)) -> rule1)) -> rule4))]
Fiona is kind.
("Fiona" "is" "kind" "+")
triple1
((triple2 triple3) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple7) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple2 triple3) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple5) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple2 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((((triple2 triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4