Fiona is smart. Gary is rough. Harry is big. If something is smart then it is red. White things are big. If Gary is white then Gary is smart. Red, rough things are white. All rough things are young. All young, rough things are big. If something is round then it is smart. Big things are round.
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Gary is white then Gary is smart.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "+"))
Red, rough things are white.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
All young, rough things are big.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Fiona is smart.
True
1
proof
[(triple1)]
("Fiona" "is" "smart" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "smart" "-")
triple1
Gary is young.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "young" "+")
((triple2) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Fiona" "is" "red" "-")
((triple1) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Fiona is smart.[(triple1)] Gary is rough.[(triple2)] Harry is big.[(triple3)] @1: Fiona is red.[(((triple1) -> rule1))] Gary is young.[(((triple2) -> rule5))] Harry is round.[(((triple3) -> rule8))] @2: Gary is big.[(((((triple2) -> rule5) triple2) -> rule6))] Harry is smart.[(((((triple3) -> rule8)) -> rule7))] @3: Gary is round.[(((((((triple2) -> rule5) triple2) -> rule6)) -> rule8))] Harry is red.[(((((((triple3) -> rule8)) -> rule7)) -> rule1))] @4: Gary is smart.[(((((((((triple2) -> rule5) triple2) -> rule6)) -> rule8)) -> rule7))] @5: Gary is red.[(((((((((((triple2) -> rule5) triple2) -> rule6)) -> rule8)) -> rule7)) -> rule1))] @6: Gary is white.[(((((((((((((triple2) -> rule5) triple2) -> rule6)) -> rule8)) -> rule7)) -> rule1) triple2) -> rule4))]
Fiona is smart.
("Fiona" "is" "smart" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
((triple1) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple3) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
((((((((((triple2) -> (rule5 % int5)) triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Gary is white.
("Gary" "is" "white" "+")
((((((((((((triple2) -> (rule5 % int6)) triple2) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is young.
("Gary" "is" "young" "+")
int6